summaryrefslogtreecommitdiff
path: root/test-suite/success/Generalization.v
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/success/Generalization.v')
-rw-r--r--test-suite/success/Generalization.v13
1 files changed, 13 insertions, 0 deletions
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
new file mode 100644
index 00000000..6b503e95
--- /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.
+
+
+