564 | _ => error "term_of_dB: function type expected" |
564 | _ => error "term_of_dB: function type expected" |
565 end |
565 end |
566 | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; |
566 | term_of_dB' _ _ = error "term_of_dB: term not in normal form"; |
567 |
567 |
568 fun typing_of_term Ts e (Bound i) = |
568 fun typing_of_term Ts e (Bound i) = |
569 rtypingT_Var (e, nat_of_int i, dBtype_of_typ (nth_elem (i, Ts))) |
569 rtypingT_Var (e, nat_of_int i, dBtype_of_typ (List.nth (Ts, i))) |
570 | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of |
570 | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of |
571 Type ("fun", [T, U]) => rtypingT_App (e, dB_of_term t, |
571 Type ("fun", [T, U]) => rtypingT_App (e, dB_of_term t, |
572 dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, |
572 dBtype_of_typ T, dBtype_of_typ U, dB_of_term u, |
573 typing_of_term Ts e t, typing_of_term Ts e u) |
573 typing_of_term Ts e t, typing_of_term Ts e u) |
574 | _ => error "typing_of_term: function type expected") |
574 | _ => error "typing_of_term: function type expected") |