author | nipkow |
Tue, 12 Jan 1999 15:48:59 +0100 | |
changeset 6099 | d4866f6ff2f9 |
parent 4879 | 58656c6a3551 |
child 13220 | 62c899c77151 |
permissions | -rw-r--r-- |
1478 | 1 |
(* Title: ZF/Let |
1061 | 2 |
ID: $Id$ |
1478 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1061 | 4 |
Copyright 1995 University of Cambridge |
5 |
||
1094 | 6 |
Let expressions, and tuple pattern-matching (borrowed from HOL) |
1061 | 7 |
*) |
8 |
||
1094 | 9 |
Let = FOL + |
1061 | 10 |
|
11 |
types |
|
12 |
letbinds letbind |
|
13 |
||
14 |
consts |
|
4879
58656c6a3551
"let" is no longer restricted to FOL terms and allows any logical terms
paulson
parents:
1478
diff
changeset
|
15 |
Let :: ['a::logic, 'a => 'b] => ('b::logic) |
1061 | 16 |
|
17 |
syntax |
|
1401 | 18 |
"_bind" :: [pttrn, 'a] => letbind ("(2_ =/ _)" 10) |
19 |
"" :: letbind => letbinds ("_") |
|
20 |
"_binds" :: [letbind, letbinds] => letbinds ("_;/ _") |
|
21 |
"_Let" :: [letbinds, 'a] => 'a ("(let (_)/ in (_))" 10) |
|
1061 | 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 |