|
1061
|
1 |
(* Title: ZF/Let
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
|
4 |
Copyright 1995 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Let expressions -- borrowed from HOL
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Let = ZF +
|
|
|
10 |
|
|
|
11 |
types
|
|
|
12 |
letbinds letbind
|
|
|
13 |
|
|
|
14 |
consts
|
|
|
15 |
Let :: "['a, 'a => 'b] => 'b"
|
|
|
16 |
|
|
|
17 |
syntax
|
|
|
18 |
"_bind" :: "[idt, 'a] => letbind" ("(2_ =/ _)" 10)
|
|
|
19 |
"" :: "letbind => letbinds" ("_")
|
|
|
20 |
"_binds" :: "[letbind, letbinds] => letbinds" ("_;/ _")
|
|
|
21 |
"_Let" :: "[letbinds, 'a] => 'a" ("(let (_)/ in (_))" 10)
|
|
|
22 |
|
|
|
23 |
translations
|
|
|
24 |
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
|
|
|
25 |
"let x = a in e" == "Let(a, %x. e)"
|
|
|
26 |
|
|
|
27 |
defs
|
|
|
28 |
Let_def "Let(s, f) == f(s)"
|
|
|
29 |
|
|
|
30 |
end
|