equal
deleted
inserted
replaced
21 translations |
21 translations |
22 "A |- e :: t" == "(A,e,t):has_type" |
22 "A |- e :: t" == "(A,e,t):has_type" |
23 |
23 |
24 inductive has_type |
24 inductive has_type |
25 intrs |
25 intrs |
26 VarI "[| n < length A; t <| (nth n A) |] ==> A |- Var n :: t" |
26 VarI "[| n < length A; t <| A!n |] ==> A |- Var n :: t" |
27 AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2" |
27 AbsI "[| (mk_scheme t1)#A |- e :: t2 |] ==> A |- Abs e :: t1 -> t2" |
28 AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] |
28 AppI "[| A |- e1 :: t2 -> t1; A |- e2 :: t2 |] |
29 ==> A |- App e1 e2 :: t1" |
29 ==> A |- App e1 e2 :: t1" |
30 LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t" |
30 LETI "[| A |- e1 :: t1; (gen A t1)#A |- e2 :: t |] ==> A |- LET e1 e2 :: t" |
31 |
31 |