commit by user andrea

[helm.git] / weblib / While / semantics.ma

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index 638b7ac912797284c79183abe310d0c5df90d6b1..ee4362b71ccd197ce70a660c9f8c9b95a27b0d39 100644 (file)
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -14,10 +14,8 @@ definition eqvar ≝ λv1,v2.
 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
@@ -30,7 +28,7 @@ let rec evalA a s ≝
  .
 
 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