29 lines
414 B
Text
29 lines
414 B
Text
|
open nat
|
||
|
|
|
||
|
|
structure foo [class] :=
|
||
|
|
(a : nat) (b : nat)
|
||
|
|
|
||
|
|
definition i1 [instance] [priority default-2] : foo :=
|
||
|
|
foo.mk 1 1
|
||
|
|
|
||
|
|
example : foo.a = 1 :=
|
||
|
|
rfl
|
||
|
|
|
||
|
|
definition i2 [instance] [priority default-1] : foo :=
|
||
|
|
foo.mk 2 2
|
||
|
|
|
||
|
|
example : foo.a = 2 :=
|
||
|
|
rfl
|
||
|
|
|
||
|
|
definition i3 [instance] : foo :=
|
||
|
|
foo.mk 3 3
|
||
|
|
|
||
|
|
example : foo.a = 3 :=
|
||
|
|
rfl
|
||
|
|
|
||
|
|
definition i4 [instance] [priority default-1] : foo :=
|
||
|
|
foo.mk 4 4
|
||
|
|
|
||
|
|
example : foo.a = 3 :=
|
||
|
|
rfl
|