From 8530992b72238902faae5e8bff74550fd8d7264a Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 7 Nov 2005 13:52:50 +0000
Subject: [PATCH] Syntactic change: [ ... ] match t in t with ==> match t in t
return ... with
---
helm/matita/library/logic/connectives.ma | 3 +--
helm/matita/library/logic/equality.ma | 3 +--
helm/matita/library/nat/minimization.ma | 4 ++--
helm/matita/matita.lang | 1 +
4 files changed, 5 insertions(+), 6 deletions(-)
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 @@
<keyword>qed</keyword>
<keyword>rec</keyword>
<keyword>record</keyword>
+ <keyword>return</keyword>
<keyword>to</keyword>
<keyword>using</keyword>
<keyword>with</keyword>
--
2.39.5