From 35093b10bc1784ebbdf2f1d61bdc84b83a3e8929 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 15:24:24 +0000 Subject: [PATCH] 1. syntax of match changed 2. syntax of the bindings of "let rec" made lighter --- helm/matita/tests/match.ma | 22 +++++++++++----------- 1 file changed, 11 insertions(+), 11 deletions(-) diff --git a/helm/matita/tests/match.ma b/helm/matita/tests/match.ma index 21bad46a9..2382ba7b7 100644 --- a/helm/matita/tests/match.ma +++ b/helm/matita/tests/match.ma @@ -98,8 +98,8 @@ qed. definition plus : nat \to nat \to nat \def -let rec plus (n,m:nat) \def - match n:nat with +let rec plus (n,m) \def + match n with [ O \Rightarrow m | (S p) \Rightarrow S (plus p m) ] in @@ -124,8 +124,8 @@ intros.elim n.simplify.apply refl_equal.simplify.apply f_equal.assumption. qed. definition times : nat \to nat \to nat \def -let rec times (n,m:nat) \def - match n:nat with +let rec times (n,m) \def + match n with [ O \Rightarrow O | (S p) \Rightarrow (plus m (times p m)) ] in @@ -152,11 +152,11 @@ simplify.elim (sym_eq ? ? ? H).apply times_n_Sm. qed. definition minus : nat \to nat \to nat \def -let rec minus (n,m:nat) \def - [\lambda n:nat.nat] match n:nat with +let rec minus (n,m) \def + [\lambda n:nat.nat] match n with [ O \Rightarrow O | (S p) \Rightarrow - [\lambda n:nat.nat] match m:nat with + [\lambda n:nat.nat] match m with [O \Rightarrow (S p) | (S q) \Rightarrow minus p q ]] in @@ -271,11 +271,11 @@ apply le_S_n.assumption. qed. definition leb : nat \to nat \to bool \def -let rec leb (n,m:nat) \def - [\lambda n:nat.bool] match n:nat with +let rec leb (n,m) \def + [\lambda n:nat.bool] match n with [ O \Rightarrow true | (S p) \Rightarrow - [\lambda n:nat.bool] match m:nat with + [\lambda n:nat.bool] match m with [ O \Rightarrow false | (S q) \Rightarrow leb p q]] in leb. @@ -300,6 +300,6 @@ let square \def (times eightyone eightyone) in intro. intro. intro.intro. -normalize goal at (? ? % ?). +STOP normalize goal at (? ? % ?). -- 2.39.2