blob: e56dcef74f384d86f9d1c24a2ce6964919043b0e (
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
|
Require Program.Tactics.
Axiom foo : nat -> Prop.
Axiom fooP : forall n, foo n.
Class myClass (A: Type) :=
{
bar : A -> Prop
}.
Program Instance myInstance : myClass nat :=
{
bar := foo
}.
Class myClassP (A : Type) :=
{
super :> myClass A;
barP : forall (a : A), bar a
}.
Instance myInstanceP : myClassP nat :=
{
barP := fooP
}.
|
