equal
deleted
inserted
replaced
48 schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" |
48 schematic_lemma "PROD x:N . PROD y:N . Eq(?A,x,y) type" |
49 apply typechk |
49 apply typechk |
50 done |
50 done |
51 |
51 |
52 text "typechecking an application of fst" |
52 text "typechecking an application of fst" |
53 schematic_lemma "(lam u. split(u, %v w. v)) ` <0, succ(0)> : ?A" |
53 schematic_lemma "(lam u. split(u, \<lambda>v w. v)) ` <0, succ(0)> : ?A" |
54 apply typechk |
54 apply typechk |
55 done |
55 done |
56 |
56 |
57 text "typechecking the predecessor function" |
57 text "typechecking the predecessor function" |
58 schematic_lemma "lam n. rec(n, 0, %x y. x) : ?A" |
58 schematic_lemma "lam n. rec(n, 0, \<lambda>x y. x) : ?A" |
59 apply typechk |
59 apply typechk |
60 done |
60 done |
61 |
61 |
62 text "typechecking the addition function" |
62 text "typechecking the addition function" |
63 schematic_lemma "lam n. lam m. rec(n, m, %x y. succ(y)) : ?A" |
63 schematic_lemma "lam n. lam m. rec(n, m, \<lambda>x y. succ(y)) : ?A" |
64 apply typechk |
64 apply typechk |
65 done |
65 done |
66 |
66 |
67 (*Proofs involving arbitrary types. |
67 (*Proofs involving arbitrary types. |
68 For concreteness, every type variable left over is forced to be N*) |
68 For concreteness, every type variable left over is forced to be N*) |
77 apply typechk |
77 apply typechk |
78 apply N |
78 apply N |
79 done |
79 done |
80 |
80 |
81 text "typechecking fst (as a function object)" |
81 text "typechecking fst (as a function object)" |
82 schematic_lemma "lam i. split(i, %j k. j) : ?A" |
82 schematic_lemma "lam i. split(i, \<lambda>j k. j) : ?A" |
83 apply typechk |
83 apply typechk |
84 apply N |
84 apply N |
85 done |
85 done |
86 |
86 |
87 end |
87 end |