From 273ed08112cf9470644498dc495d9e60519e5eaa Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 10 Oct 2002 19:44:25 +0000 Subject: [PATCH] Added an example to test fourier_tac. --- helm/gTopLevel/esempi/fourier.cic | 8 ++++++++ 1 file changed, 8 insertions(+) create mode 100644 helm/gTopLevel/esempi/fourier.cic diff --git a/helm/gTopLevel/esempi/fourier.cic b/helm/gTopLevel/esempi/fourier.cic new file mode 100644 index 000000000..cae3925a7 --- /dev/null +++ b/helm/gTopLevel/esempi/fourier.cic @@ -0,0 +1,8 @@ +alias Rge /Coq/Reals/Rdefinitions/Rge.con +alias Rle /Coq/Reals/Rdefinitions/Rle.con +alias Rplus /Coq/Reals/Rdefinitions/Rplus.con +alias Rminus /Coq/Reals/Rdefinitions/Rminus.con +alias R1 /Coq/Reals/Rdefinitions/R1.con +alias R /Coq/Reals/Rdefinitions/R.con + +!x:R.!y:R.(Rle x y) -> (Rge (Rplus y R1) (Rminus x R1)) -- 2.39.2