blob: 5326c0fbb1fb4d3d43e4b1d822df255ec5a96e38 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
Class Foo := { foo : Set }.
Axiom admit : forall {T}, T.
Global Instance Foo0 : Foo
:= {| foo := admit |}.
Global Instance Foo1 : Foo
:= { foo := admit }.
Existing Class Foo.
Global Instance Foo2 : Foo
:= { foo := admit }. (* Error: Unbound method name foo of class Foo. *)
Set Warnings "+already-existing-class".
Fail Existing Class Foo.
|
