blob: 78b2aa69b9f3524a4b9be36f3db0b4cd73f8be46 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
Set Nested Proofs Allowed.
Class Foo.
Class Bar := b : Type.
Instance foo : Foo := _.
(* 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.
|
