equal
deleted
inserted
replaced
9 type_synonym state = "vname \<Rightarrow> val" |
9 type_synonym state = "vname \<Rightarrow> val" |
10 |
10 |
11 datatype aexp = N int | V vname | Plus aexp aexp |
11 datatype aexp = N int | V vname | Plus aexp aexp |
12 |
12 |
13 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where |
13 fun aval :: "aexp \<Rightarrow> state \<Rightarrow> val" where |
14 "aval (N n) _ = n" | |
14 "aval (N n) s = n" | |
15 "aval (V x) s = s x" | |
15 "aval (V x) s = s x" | |
16 "aval (Plus a1 a2) s = aval a1 s + aval a2 s" |
16 "aval (Plus a1 a2) s = aval a1 s + aval a2 s" |
17 |
17 |
18 |
18 |
19 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)" |
19 value "aval (Plus (V ''x'') (N 5)) (\<lambda>x. if x = ''x'' then 7 else 0)" |