equal
deleted
inserted
replaced
|
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 |