equal
deleted
inserted
replaced
22 datatype |
22 datatype |
23 "TyEnv" = te_emp |
23 "TyEnv" = te_emp |
24 | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty") |
24 | te_owr ("te \<in> TyEnv","x \<in> ExVar","t \<in> Ty") |
25 |
25 |
26 consts |
26 consts |
27 te_dom :: "i => i" |
27 te_dom :: "i \<Rightarrow> i" |
28 te_app :: "[i,i] => i" |
28 te_app :: "[i,i] \<Rightarrow> i" |
29 |
29 |
30 |
30 |
31 primrec (*domain of the type environment*) |
31 primrec (*domain of the type environment*) |
32 "te_dom (te_emp) = 0" |
32 "te_dom (te_emp) = 0" |
33 "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}" |
33 "te_dom (te_owr(te,x,v)) = te_dom(te) \<union> {x}" |