blob: 85d5c3e1231f27bf05dc1bdaa95e2520dfb463ad (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
(* Examples of use of Scheme Equality *)
Module A.
Definition N := nat.
Inductive list := nil | cons : N -> list -> list.
Scheme Equality for list.
End A.
Module B.
Section A.
Context A (eq_A:A->A->bool)
(A_bl : forall x y, eq_A x y = true -> x = y)
(A_lb : forall x y, x = y -> eq_A x y = true).
Inductive I := C : A -> I.
Scheme Equality for I.
End A.
End B.
Module C.
Parameter A : Type.
Parameter eq_A : A->A->bool.
Parameter A_bl : forall x y, eq_A x y = true -> x = y.
Parameter A_lb : forall x y, x = y -> eq_A x y = true.
Hint Resolve A_bl A_lb : core.
Inductive I := C : A -> I.
Scheme Equality for I.
Inductive J := D : list A -> J.
Scheme Equality for J.
End C.
|
