definition update : state → Var → nat → state ≝ λs,v,a,v1.
if eqvar v1 v then a else s v1.
-
(* Semantics of Arithmetic expressions *)
-\ 5pre class="smallmargin" style="display: inline;"\ 6
-let rec evalA a s ≝
+\ 5pre class="smallmargin" style="display: inline;"\ 6let rec evalA a s ≝
match a with
[ Const n => n
| Aid v => s v
.
example exA1: evalA ((Const 2)+(Const 3)*(Aid (Id 2))) (λx.\ 5span style="text-decoration: underline;"\ 61\ 5/span\ 6) = \ 5span style="text-decoration: underline;"\ 65\ 5/span\ 6.
-normalize // qed.
+normalize // qed
let rec evalB b s ≝
match b with