equal
deleted
inserted
replaced
19 "@has_type" :: [typ list, expr, typ] => bool |
19 "@has_type" :: [typ list, expr, typ] => bool |
20 ("((_) |-/ (_) :: (_))" [60,0,60] 60) |
20 ("((_) |-/ (_) :: (_))" [60,0,60] 60) |
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 |] ==> a |- Var n :: nth n a" |
26 VarI "[| n < length a |] ==> a |- Var n :: nth n a" |
27 AbsI "[| t1#a |- e :: t2 |] ==> a |- Abs e :: t1 -> t2" |
27 AbsI "[| 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" |