From 5433a131a7ff29529747e58c68dbf258d696e55b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Wed, 5 Oct 2005 09:04:43 +0000 Subject: [PATCH] separated "]]" to avoid clash with (temporary) continuationals ligatures --- helm/matita/library/Z/plus.ma | 4 ++-- helm/matita/library/nat/gcd.ma | 4 ++-- helm/matita/library/nat/ord.ma | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) diff --git a/helm/matita/library/Z/plus.ma b/helm/matita/library/Z/plus.ma index 0456ca0b3..c1db18b18 100644 --- a/helm/matita/library/Z/plus.ma +++ b/helm/matita/library/Z/plus.ma @@ -29,7 +29,7 @@ definition Zplus :Z \to Z \to Z \def match nat_compare m n with [ LT \Rightarrow (neg (pred (n-m))) | EQ \Rightarrow OZ - | GT \Rightarrow (pos (pred (m-n)))]] + | GT \Rightarrow (pos (pred (m-n)))] ] | (neg m) \Rightarrow match y with [ OZ \Rightarrow x @@ -38,7 +38,7 @@ definition Zplus :Z \to Z \to Z \def [ LT \Rightarrow (pos (pred (n-m))) | EQ \Rightarrow OZ | GT \Rightarrow (neg (pred (m-n)))] - | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))]]. + | (neg n) \Rightarrow (neg (pred ((S m)+(S n))))] ]. (*CSC: the URI must disappear: there is a bug now *) interpretation "integer plus" 'plus x y = (cic:/matita/Z/plus/Zplus.con x y). diff --git a/helm/matita/library/nat/gcd.ma b/helm/matita/library/nat/gcd.ma index eb1053feb..90de2013a 100644 --- a/helm/matita/library/nat/gcd.ma +++ b/helm/matita/library/nat/gcd.ma @@ -115,7 +115,7 @@ match leb n m with | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides m + | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides m \land match leb n m with [ true \Rightarrow @@ -125,7 +125,7 @@ match leb n m with | false \Rightarrow match m with [ O \Rightarrow n - | (S p) \Rightarrow gcd_aux (S p) n (S p) ]] \divides n. + | (S p) \Rightarrow gcd_aux (S p) n (S p) ] ] \divides n. apply leb_elim n m. apply nat_case1 n. simplify.intros.split. diff --git a/helm/matita/library/nat/ord.ma b/helm/matita/library/nat/ord.ma index d0e2b98f0..1992121b6 100644 --- a/helm/matita/library/nat/ord.ma +++ b/helm/matita/library/nat/ord.ma @@ -28,7 +28,7 @@ let rec p_ord_aux p n m \def [ O \Rightarrow pair nat nat O n | (S p) \Rightarrow match (p_ord_aux p (n / m) m) with - [ (pair q r) \Rightarrow pair nat nat (S q) r]] + [ (pair q r) \Rightarrow pair nat nat (S q) r] ] | (S a) \Rightarrow pair nat nat O n]. (* p_ord n m = if m divides n q times, with remainder r *) -- 2.39.2