equal
deleted
inserted
replaced
1 theory BExp imports AExp begin |
1 theory BExp imports AExp begin |
2 |
2 |
3 subsection "Boolean Expressions" |
3 subsection "Boolean Expressions" |
4 |
4 |
5 datatype_new bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
5 datatype bexp = Bc bool | Not bexp | And bexp bexp | Less aexp aexp |
6 |
6 |
7 text_raw{*\snip{BExpbvaldef}{1}{2}{% *} |
7 text_raw{*\snip{BExpbvaldef}{1}{2}{% *} |
8 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
8 fun bval :: "bexp \<Rightarrow> state \<Rightarrow> bool" where |
9 "bval (Bc v) s = v" | |
9 "bval (Bc v) s = v" | |
10 "bval (Not b) s = (\<not> bval b s)" | |
10 "bval (Not b) s = (\<not> bval b s)" | |