equal
deleted
inserted
replaced
8 |
8 |
9 State = WellType + |
9 State = WellType + |
10 |
10 |
11 consts |
11 consts |
12 the_Bool :: "val \\<Rightarrow> bool" |
12 the_Bool :: "val \\<Rightarrow> bool" |
13 the_Int :: "val \\<Rightarrow> int" |
13 the_Intg :: "val \\<Rightarrow> int" |
14 the_Addr :: "val \\<Rightarrow> loc" |
14 the_Addr :: "val \\<Rightarrow> loc" |
15 |
15 |
16 defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *) |
16 defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *) |
17 default_val :: "ty \\<Rightarrow> val" (* default value for all types *) |
17 default_val :: "ty \\<Rightarrow> val" (* default value for all types *) |
18 |
18 |
19 primrec |
19 primrec |
20 "the_Bool (Bool b) = b" |
20 "the_Bool (Bool b) = b" |
21 |
21 |
22 primrec |
22 primrec |
23 "the_Int (Intg i) = i" |
23 "the_Intg (Intg i) = i" |
24 |
24 |
25 primrec |
25 primrec |
26 "the_Addr (Addr a) = a" |
26 "the_Addr (Addr a) = a" |
27 |
27 |
28 primrec |
28 primrec |