From 57cb1648fcf7da18d74c28a4d63d59ea129ab136 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 23 Oct 2008 12:49:34 +0000
Subject: Generalized implementation of generalization. - New constr_expr
 construct [CGeneralization of loc * binding_kind * abstraction_kind option *
 constr_expr] to generalize the free vars of the [constr_expr], binding these
 using [binding_kind] and making a lambda or a pi (or deciding from the scope)
 using [abstraction_kind option] (abstraction_kind = AbsLambda | AbsPi) -
 Concrete syntax "`( a = 0 )" for explicit binding of [a] and "`{ ... }" for
 implicit bindings (both "..(" and "_(" seem much more difficult to
 implement). Subject to discussion! A few examples added in a test-suite file.
 - Also add missing syntax for implicit/explicit combinations for _binders_:
 "{( )}" means implicit for the generalized (outer) vars, explicit for the
 (inner) variable itself. Subject to discussion as well :) - Factor much
 typeclass instance declaration code. We now just have to force generalization
 of the term after the : in instance declarations. One more step to using
 Instance for records.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11495 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Generalization.v | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 test-suite/success/Generalization.v

(limited to 'test-suite')

diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
new file mode 100644
index 0000000000..d86d34d351
--- /dev/null
+++ b/test-suite/success/Generalization.v
@@ -0,0 +1,13 @@
+
+Check `(a = 0).
+Check `(a = 0)%type.
+Definition relation A := A -> A -> Prop.
+Definition equivalence {(R : relation A)} := True.
+Check (`(@equivalence A R)).
+
+Definition a_eq_b : `( a = 0 /\ a = b /\ b > c \/ d = e /\ d = 1).
+Admitted.
+Print a_eq_b.
+
+
+
-- 
cgit v1.2.3