(* *)
(**************************************************************************)
-include "basic_2/grammar/term_vector.ma".
-include "basic_2/grammar/genv.ma".
+include "basic_2/syntax/term_vector.ma".
+include "basic_2/syntax/genv.ma".
+include "apps_2/functional/notation.ma".
(* REDUCTION AND TYPE MACHINE ***********************************************)
(* initial state *)
definition rtm_i: genv → term → rtm ≝
- λG,T. mk_rtm G 0 (â\8b\86) (â\9f ) T.
+ λG,T. mk_rtm G 0 (â\8b\86) (â\97\8a) T.
(* update code *)
definition rtm_t: rtm → term → rtm ≝
λM,T. match M with
- [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\9f ) T
+ [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\97\8a) T
].
(* update closure *)
definition rtm_u: rtm → xenv → term → rtm ≝
λM,E,T. match M with
- [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\9f ) T
+ [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\97\8a) T
].
(* get global environment *)