blob: 9d83743b2a90b8d76e36af528c9220ddc408b40b (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Set Nested Proofs Allowed.
Class Foo.
Class Bar := b : Type.
Set Refine Instance Mode.
Instance foo : Foo := _.
Unset Refine Instance Mode.
(* 1 subgoals, subgoal 1 (ID 4)
============================
Foo *)
Instance bar : Bar.
exact Type.
Defined.
(* bar is defined *)
About foo.
(* foo not a defined object. *)
Fail Defined.
|
