26 succ :: "i=>i" |
26 succ :: "i=>i" |
27 ncase :: "[i,i,i=>i]=>i" |
27 ncase :: "[i,i,i=>i]=>i" |
28 nrec :: "[i,i,[i,i]=>i]=>i" |
28 nrec :: "[i,i,[i,i]=>i]=>i" |
29 |
29 |
30 nil :: "i" ("([])") |
30 nil :: "i" ("([])") |
31 "." :: "[i,i]=>i" (infixr 80) |
31 "$" :: "[i,i]=>i" (infixr 80) |
32 lcase :: "[i,i,[i,i]=>i]=>i" |
32 lcase :: "[i,i,[i,i]=>i]=>i" |
33 lrec :: "[i,i,[i,i,i]=>i]=>i" |
33 lrec :: "[i,i,[i,i,i]=>i]=>i" |
34 |
34 |
35 let :: "[i,i=>i]=>i" |
35 let :: "[i,i=>i]=>i" |
36 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
36 letrec :: "[[i,i=>i]=>i,(i=>i)=>i]=>i" |
58 zero_def "zero == inl(one)" |
58 zero_def "zero == inl(one)" |
59 succ_def "succ(n) == inr(n)" |
59 succ_def "succ(n) == inr(n)" |
60 ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))" |
60 ncase_def "ncase(n,b,c) == when(n,%x.b,%y.c(y))" |
61 nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)" |
61 nrec_def " nrec(n,b,c) == letrec g x be ncase(x,b,%y.c(y,g(y))) in g(n)" |
62 nil_def "[] == inl(one)" |
62 nil_def "[] == inl(one)" |
63 cons_def "h.t == inr(<h,t>)" |
63 cons_def "h$t == inr(<h,t>)" |
64 lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))" |
64 lcase_def "lcase(l,b,c) == when(l,%x.b,%y.split(y,c))" |
65 lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)" |
65 lrec_def "lrec(l,b,c) == letrec g x be lcase(x,b,%h t.c(h,t,g(t))) in g(l)" |
66 |
66 |
67 let_def "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))" |
67 let_def "let x be t in f(x) == case(t,f(true),f(false),%x y.f(<x,y>),%u.f(lam x.u(x)))" |
68 letrec_def |
68 letrec_def |