38 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
38 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
39 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
39 letrec2 :: "[[i,i,i=>i=>i]=>i,(i=>i=>i)=>i]=>i" |
40 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
40 letrec3 :: "[[i,i,i,i=>i=>i=>i]=>i,(i=>i=>i=>i)=>i]=>i" |
41 |
41 |
42 syntax |
42 syntax |
43 "_let" :: "[idt,i,i]=>i" ("(3let _ be _/ in _)" |
43 "_let" :: "[id,i,i]=>i" ("(3let _ be _/ in _)" |
44 [0,0,60] 60) |
44 [0,0,60] 60) |
45 |
45 |
46 "_letrec" :: "[idt,idt,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
46 "_letrec" :: "[id,id,i,i]=>i" ("(3letrec _ _ be _/ in _)" |
47 [0,0,0,60] 60) |
47 [0,0,0,60] 60) |
48 |
48 |
49 "_letrec2" :: "[idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
49 "_letrec2" :: "[id,id,id,i,i]=>i" ("(3letrec _ _ _ be _/ in _)" |
50 [0,0,0,0,60] 60) |
50 [0,0,0,0,60] 60) |
51 |
51 |
52 "_letrec3" :: "[idt,idt,idt,idt,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
52 "_letrec3" :: "[id,id,id,id,i,i]=>i" ("(3letrec _ _ _ _ be _/ in _)" |
53 [0,0,0,0,0,60] 60) |
53 [0,0,0,0,0,60] 60) |
54 |
54 |
55 ML {* |
55 ML {* |
56 (** Quantifier translations: variable binding **) |
56 (** Quantifier translations: variable binding **) |
57 |
57 |