blob: f4d2f07db5763360419891db06559b56983c451b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
Class Foo := foo { a : nat; b : bool }.
Fail Instance bla : Foo := { b:= true }.
#[refine] Instance bla : Foo := { b:= true }.
Proof.
exact 0.
Defined.
Instance bli : Foo := { a:=1; b := false}.
Check bli.
Fail #[program, refine] Instance bla : Foo := {b := true}.
#[program] Instance blo : Foo := {b := true}.
Next Obligation. exact 2. Qed.
Check blo.
#[refine] Instance xbar : Foo := {a:=4; b:=true}.
Proof. Qed.
Check xbar.
|
