equal
deleted
inserted
replaced
10 |
10 |
11 consts |
11 consts |
12 I :: [expr, typ list, nat, subst] => result_W |
12 I :: [expr, typ list, nat, subst] => result_W |
13 |
13 |
14 primrec I expr |
14 primrec I expr |
15 "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n) |
15 "I (Var i) a n s = (if i < length a then Ok(s, a!i, n) |
16 else Fail)" |
16 else Fail)" |
17 "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s; |
17 "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s; |
18 Ok(s, TVar n -> t, m) )" |
18 Ok(s, TVar n -> t, m) )" |
19 "I (App e1 e2) a n s = |
19 "I (App e1 e2) a n s = |
20 ( (s1,t1,m1) := I e1 a n s; |
20 ( (s1,t1,m1) := I e1 a n s; |