equal
deleted
inserted
replaced
9 "bval (Not b) s = (\<not> bval b s)" | |
9 "bval (Not b) s = (\<not> bval b s)" | |
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
10 "bval (And b1 b2) s = (if bval b1 s then bval b2 s else False)" | |
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
11 "bval (Less a1 a2) s = (aval a1 s < aval a2 s)" |
12 |
12 |
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
13 value "bval (Less (V ''x'') (Plus (N 3) (V ''y''))) |
14 (lookup [(''x'',3),(''y'',1)])" |
14 [''x'' \<rightarrow> 3, ''y'' \<rightarrow> 1]" |
15 |
15 |
16 |
16 |
17 subsection "Optimization" |
17 subsection "Optimization" |
18 |
18 |
19 text{* Optimized constructors: *} |
19 text{* Optimized constructors: *} |