From 87b143efa63a920f7e36d2590ee23a45f450dfce Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Nov 2002 12:45:25 +0000 Subject: [PATCH] - Comments updated - Eq renamed to eqT --- helm/gTopLevel/esempi/fourier.cic | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic index 09caea79b..a76b4586a 100644 --- a/helm/gTopLevel/esempi/fourier.cic +++ b/helm/gTopLevel/esempi/fourier.cic @@ -9,7 +9,7 @@ alias Rminus /Coq/Reals/Rdefinitions/Rminus.con alias R1 /Coq/Reals/Rdefinitions/R1.con alias R0 /Coq/Reals/Rdefinitions/R0.con alias R /Coq/Reals/Rdefinitions/R.con -alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1 +alias eqT /Coq/Init/Logic_Type/eqT.ind#1/1 //test base1 ok !x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) @@ -17,7 +17,7 @@ alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1 //test base2 ok !x:R.!y:R.(Rlt x y) -> (Rgt (Rplus y R1) (Rminus x R1)) -//test base3 (unification fails) +//test base3 ok !x:R.!y:R.(Rge x y) -> (Rlt (Rplus y R1) (Rplus x (Rplus R1 R1))) //test base4 ok @@ -26,8 +26,8 @@ alias Eq /Coq/Init/Logic_Type/eqT.ind#1/1 //test base5 ok !x:R.!y:R.(Rlt x ( Rplus y R1 ) ) -> (Rge (Rplus y (Rplus R1 R1)) (Rminus x R0)) -//test base6 (unification fails) -!x:R.!y:R.(Eq R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) +//test base6 (fourier fails) +!x:R.!y:R.(eqT R x y) -> (Rgt (Rplus y R1) (Rminus x R1)) //test base7 (should fail) ok !x:R.!y:R.(Rlt x y) -> (Rlt (Rplus y R1) (Rminus x R1)) -- 2.39.2