equal
deleted
inserted
replaced
24 where "the_Intg (Intg i) = i" |
24 where "the_Intg (Intg i) = i" |
25 |
25 |
26 primrec the_Addr :: "val \<Rightarrow> loc" |
26 primrec the_Addr :: "val \<Rightarrow> loc" |
27 where "the_Addr (Addr a) = a" |
27 where "the_Addr (Addr a) = a" |
28 |
28 |
29 types dyn_ty = "loc \<Rightarrow> ty option" |
29 type_synonym dyn_ty = "loc \<Rightarrow> ty option" |
30 |
30 |
31 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
31 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
32 where |
32 where |
33 "typeof dt Unit = Some (PrimT Void)" |
33 "typeof dt Unit = Some (PrimT Void)" |
34 | "typeof dt (Bool b) = Some (PrimT Boolean)" |
34 | "typeof dt (Bool b) = Some (PrimT Boolean)" |