From f8404e07a6b8649e85bf7a4f812a382cd3a37fca Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 28 Jul 2005 09:00:22 +0000 Subject: [PATCH] More notation. --- helm/matita/library/Z/z.ma | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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). -- 2.39.2