aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Generalization.v
blob: d86d34d351b83ce413f9d7053638d76faf58657e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
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.