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 patternmatching (borrowed from HOL)

1061

7 
*)


8 

1094

9 
Let = FOL +

1061

10 


11 
types


12 
letbinds letbind


13 


14 
consts

1401

15 
Let :: ['a, 'a => 'b] => 'b

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
