From: matitaweb Date: Wed, 10 Apr 2013 11:44:22 +0000 (+0000) Subject: commit by user andrea X-Git-Tag: make_still_working~1192 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bcbd3124423b5e95855da2a34a126b59caa9a3f8;p=helm.git commit by user andrea --- diff --git a/weblib/While/syntax.ma b/weblib/While/syntax.ma index 95c93c7e4..8b77cab88 100644 --- a/weblib/While/syntax.ma +++ b/weblib/While/syntax.ma @@ -23,7 +23,7 @@ inductive Aexp : Type[0] ≝ . interpretation "Aexp plus" 'plus x y = (Add x y). -interpretation "Aexp minus" 'plus x y = (Sub x y). +interpretation "Aexp minus" 'minus x y = (Sub x y). interpretation "Aexp times" 'times x y = (Mul x y). (* Boolean expressions *)