(* initial state *)
definition rtm_i: genv → term → rtm ≝
- λG,T. mk_rtm G 0 (â\8b\86) (â\97\8a) T.
+ λG,T. mk_rtm G 0 (â\8b\86) (â\92º) 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 (â\97\8a) T
+ [ mk_rtm G u E _ _ â\87\92 mk_rtm G u E (â\92º) 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 (â\97\8a) T
+ [ mk_rtm G u _ _ _ â\87\92 mk_rtm G u E (â\92º) T
].
(* get global environment *)