From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 09:00:22 +0000 (+0000) Subject: More notation. X-Git-Tag: V_0_7_2~29 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f8404e07a6b8649e85bf7a4f812a382cd3a37fca;p=helm.git More notation. --- diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index 118cdd55e..d3bc2ee25 100644 --- a/helm/matita/library/Z/z.ma +++ b/helm/matita/library/Z/z.ma @@ -108,21 +108,21 @@ definition Zplus :Z \to Z \to Z \def | (pos m) \Rightarrow match y with [ OZ \Rightarrow x - | (pos n) \Rightarrow (pos (S (plus m n))) + | (pos n) \Rightarrow (pos (S (m+n))) | (neg n) \Rightarrow match nat_compare m n with - [ LT \Rightarrow (neg (pred (minus n m))) + [ LT \Rightarrow (neg (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (pos (pred (minus m n)))]] + | GT \Rightarrow (pos (pred (m-n)))]] | (neg m) \Rightarrow match y with [ OZ \Rightarrow x | (pos n) \Rightarrow match nat_compare m n with - [ LT \Rightarrow (pos (pred (minus n m))) + [ LT \Rightarrow (pos (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (neg (pred (minus m n)))] - | (neg n) \Rightarrow (neg (S (plus m n)))]]. + | GT \Rightarrow (neg (pred (m-n)))] + | (neg n) \Rightarrow (neg (S (m+n)))]]. (*CSC: the URI must disappear: there is a bug now *) interpretation "integer plus" 'plus x y = (cic:/matita/Z/z/Zplus.con x y).