49 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i" |
49 definition "let1" :: "[i,i\<Rightarrow>i]\<Rightarrow>i" |
50 where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))" |
50 where let_def: "let1(t, f) == case(t,f(true),f(false), \<lambda>x y. f(<x,y>), \<lambda>u. f(lam x. u(x)))" |
51 |
51 |
52 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" |
52 syntax "_let1" :: "[idt,i,i]\<Rightarrow>i" |
53 (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60) |
53 (\<open>(\<open>indent=3 notation=\<open>mixfix let be in\<close>\<close>let _ be _/ in _)\<close> [0,0,60] 60) |
54 syntax_consts let1 |
|
55 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)" |
54 translations "let x be a in e" == "CONST let1(a, \<lambda>x. e)" |
56 |
55 |
57 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
56 definition letrec :: "[[i,i\<Rightarrow>i]\<Rightarrow>i,(i\<Rightarrow>i)\<Rightarrow>i]\<Rightarrow>i" |
58 where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)" |
57 where "letrec(h, b) == b(\<lambda>x. fix(\<lambda>f. lam x. h(x,\<lambda>y. f`y))`x)" |
59 |
58 |
71 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ be _/ in _)\<close> [0,0,0,60] 60) |
70 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ be _/ in _)\<close> [0,0,0,60] 60) |
72 "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" |
71 "_letrec2" :: "[idt,idt,idt,i,i]\<Rightarrow>i" |
73 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60) |
72 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ be _/ in _)\<close> [0,0,0,0,60] 60) |
74 "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" |
73 "_letrec3" :: "[idt,idt,idt,idt,i,i]\<Rightarrow>i" |
75 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60) |
74 (\<open>(\<open>indent=3 notation=\<open>mixfix letrec be in\<close>\<close>letrec _ _ _ _ be _/ in _)\<close> [0,0,0,0,0,60] 60) |
76 syntax_consts letrec letrec2 letrec3 |
|
77 parse_translation \<open> |
75 parse_translation \<open> |
78 let |
76 let |
79 fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; |
77 fun abs_tr t u = Syntax_Trans.abs_tr [t, u]; |
80 fun letrec_tr [f, x, a, b] = |
78 fun letrec_tr [f, x, a, b] = |
81 Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b; |
79 Syntax.const \<^const_syntax>\<open>letrec\<close> $ abs_tr x (abs_tr f a) $ abs_tr f b; |