From c8aa73f573026ca9e1736f058bf77561f028c10a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 16:36:55 +0000 Subject: [PATCH] Syntax for top-level "let rec" fixed. --- helm/matita/tests/coercions.ma | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/matita/tests/coercions.ma b/helm/matita/tests/coercions.ma index 21bf994ce..3d1279133 100644 --- a/helm/matita/tests/coercions.ma +++ b/helm/matita/tests/coercions.ma @@ -26,7 +26,7 @@ coercion pos2nat. coercion nat2int. -let rec plus (x,y:int) on x : int \def +let rec plus x y : int \def match x with [ (positive n) \Rightarrow x | (negative z) \Rightarrow y]. -- 2.39.2