From da5cf21f33e7303bf9b1fc60470de1f6101714dd Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 12 Dec 2011 16:35:41 +0000 Subject: [PATCH] Parentheses are now needed. I do not know why and when this has changed. --- matita/matita/lib/arithmetics/primes.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/matita/matita/lib/arithmetics/primes.ma b/matita/matita/lib/arithmetics/primes.ma index 7c5df29f3..c8b2a25bf 100644 --- a/matita/matita/lib/arithmetics/primes.ma +++ b/matita/matita/lib/arithmetics/primes.ma @@ -439,9 +439,9 @@ let rec nth_prime n ≝ match n with min upper_bound (S previous_prime) primeb]. lemma nth_primeS: ∀n.nth_prime (S n) = - let previous_prime ≝ nth_prime n in + (let previous_prime ≝ nth_prime n in let upper_bound ≝ S previous_prime! in - min upper_bound (S previous_prime) primeb. + min upper_bound (S previous_prime) primeb). // qed. (* it works *) -- 2.39.2