From: matitaweb <claudio.sacerdoticoen@unibo.it>
Date: Wed, 10 Apr 2013 11:43:43 +0000 (+0000)
Subject: commit by user andrea
X-Git-Tag: make_still_working~1193
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=ef335c7310bd175a2df936eb284fed6142ee0b6e

commit by user andrea
---

diff --git a/weblib/While/semantics.ma b/weblib/While/semantics.ma
index ec11cf2ec..5898be246 100644
--- a/weblib/While/semantics.ma
+++ b/weblib/While/semantics.ma
@@ -1,29 +1,29 @@
 (* new script *)
 
 include "While/syntax.ma". 
-include "arithmetics/div_and_mod.ma. 
+include "arithmetics/div_and_mod.ma". 
 
 
 (* state *)
 
-definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
+img class="anchor" src="icons/tick.png" id="state"definition state ≝ a href="cic:/matita/While/syntax/Var.ind(1,0,0)"Var/a → a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.
 
 (* Semantics of Arithmetic expressions *)
 
-pre class="smallmargin" style="display: inline;"let rec eval_Aexp a s ≝
+pre class="smallmargin" style="display: inline;"img class="anchor" src="icons/tick.png" id="evalA"let rec evalA a s ≝
   match a with 
-  | Const n => n
+  [ Const n => n
   | Aid v => s v
-  | Add a b => a+b
-  | Sub a b => a-b
-  | Mul a b => a*b
-  | Div a b => div a b
-  | Mod a b => mod a b
+  | Add a b => evalA a sa title="natural plus" href="cic:/fakeuri.def(1)"+/aevalA b s
+  | Sub a b => evalA a sa title="natural minus" href="cic:/fakeuri.def(1)"-/aevalA b s
+  | Mul a b => evalA a sa title="natural times" href="cic:/fakeuri.def(1)"*/aevalA b s
+  | Div a b => a href="cic:/matita/arithmetics/div_and_mod/div.def(3)"div/a (evalA a s) (evalA b s)
+  | Mod a b => a href="cic:/matita/arithmetics/div_and_mod/mod.def(3)"mod/a (evalA a s) (evalA b s) 
+  ]
  .
 
-interpretation "Aexp plus" 'plus x y = (Add x y).
-interpretation "Aexp minus" 'plus x y = (Sub x y).
-interpretation "Aexp times" 'times x y = (Mul x y).
+img class="anchor" src="icons/tick.png" id="exA1"example exA1: a href="cic:/matita/While/semantics/evalA.fix(0,0,4)"evalA/a ((a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"2/a)a href="cic:/fakeuri.def(1)" title="Aexp plus"+/a(a href="cic:/matita/While/syntax/Aexp.con(0,1,0)"Const/a a title="natural number" href="cic:/fakeuri.def(1)"3/a)) (λx.a title="natural number" href="cic:/fakeuri.def(1)"0/a) a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a title="natural number" href="cic:/fakeuri.def(1)"5/a.
+normalize ///pre. 
 
 (* Boolean expressions *)
 inductive Bexp : Type[0] ≝
@@ -50,4 +50,4 @@ inductive Cmd : Type[0] ≝
   | While : a href="cic:/matita/While/syntax/Bexp.ind(1,0,0)"Bexp/a → Cmd → Cmd
 .
 
-/pre 
\ No newline at end of file
+ 
\ No newline at end of file