From: Claudio Sacerdoti Coen Date: Mon, 7 Nov 2005 13:52:50 +0000 (+0000) Subject: Syntactic change: X-Git-Tag: V_0_7_2_3~115 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8530992b72238902faae5e8bff74550fd8d7264a;p=helm.git Syntactic change: [ ... ] match t in t with ==> match t in t return ... with --- diff --git a/helm/matita/library/logic/connectives.ma b/helm/matita/library/logic/connectives.ma index 2848c08c5..4cbea3529 100644 --- a/helm/matita/library/logic/connectives.ma +++ b/helm/matita/library/logic/connectives.ma @@ -65,8 +65,7 @@ theorem Or_ind': \forall p:A \lor B. P p. intros. apply - ([\lambda p.P p] - match p with + (match p return \lambda p.P p with [(or_introl p) \Rightarrow H p |(or_intror q) \Rightarrow H1 q]). qed. diff --git a/helm/matita/library/logic/equality.ma b/helm/matita/library/logic/equality.ma index 7e67c056c..40157d849 100644 --- a/helm/matita/library/logic/equality.ma +++ b/helm/matita/library/logic/equality.ma @@ -32,8 +32,7 @@ theorem eq_ind': P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p. intros. exact - ([\lambda y. \lambda p.P y p] - match p with + (match p return \lambda y. \lambda p.P y p with [refl_eq \Rightarrow H]). qed. diff --git a/helm/matita/library/nat/minimization.ma b/helm/matita/library/nat/minimization.ma index 94e4ee367..0abed5ad3 100644 --- a/helm/matita/library/nat/minimization.ma +++ b/helm/matita/library/nat/minimization.ma @@ -85,7 +85,7 @@ apply (le_n_O_elim a H2).intro.simplify.rewrite > H4. simplify.assumption. simplify. apply (bool_ind (\lambda b:bool. -(f (S n1) = b) \to (f ([\lambda b:bool.nat] match b in bool with +(f (S n1) = b) \to (f (match b in bool with [ true \Rightarrow (S n1) | false \Rightarrow (max n1 f)])) = true)). simplify.intro.assumption. @@ -160,7 +160,7 @@ rewrite > (min_aux_O_f f).rewrite < Hcut.assumption. apply (antisym_le a m).assumption.rewrite > (minus_n_O m).assumption. simplify. apply (bool_ind (\lambda b:bool. -(f (m-(S n)) = b) \to (f ([\lambda b:bool.nat] match b in bool with +(f (m-(S n)) = b) \to (f (match b in bool with [ true \Rightarrow m-(S n) | false \Rightarrow (min_aux n m f)])) = true)). simplify.intro.assumption. diff --git a/helm/matita/matita.lang b/helm/matita/matita.lang index 9f917d0b3..3241d239e 100644 --- a/helm/matita/matita.lang +++ b/helm/matita/matita.lang @@ -44,6 +44,7 @@ qed rec record + return to using with