From d8cf90b2aa66f0170db0c35b8b5d53a1eb74008e Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 16:49:40 +0000 Subject: [PATCH] Let's try to make the "let rec" construct infer its arguments. --- helm/matita/tests/coercions.ma | 6 +++--- helm/matita/tests/letrec.ma | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 3d1279133..9e47c3e1e 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -12,12 +12,12 @@ inductive int: Set \def inductive empty : Set \def . -let rec pos2nat (x:pos) : nat \def +let rec pos2nat x \def match x with [ one \Rightarrow (S O) | (next z) \Rightarrow S (pos2nat z)]. -let rec nat2int (x:nat) :int \def +let rec nat2int x \def match x with [ O \Rightarrow positive O | (S z) \Rightarrow positive (S z)]. @@ -26,7 +26,7 @@ coercion pos2nat. coercion nat2int. -let rec plus x y : int \def +let rec plus x y \def match x with [ (positive n) \Rightarrow x | (negative z) \Rightarrow y]. diff --git a/helm/matita/tests/letrec.ma b/helm/matita/tests/letrec.ma index 464f7fa21..24b63593c 100644 --- a/helm/matita/tests/letrec.ma +++ b/helm/matita/tests/letrec.ma @@ -3,7 +3,7 @@ alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". -let rec plus n m : nat \def +let rec plus n m \def match n with [ O \Rightarrow m | (S x) \Rightarrow S (plus x m) ]. -- 2.39.2