22 lines
256 B
Text
22 lines
256 B
Text
new_frontend
|
|
|
|
structure A :=
|
|
(x : Nat := 0)
|
|
|
|
def foo : A :=
|
|
{}
|
|
|
|
theorem ex1 : foo = { x := 0 } :=
|
|
rfl
|
|
|
|
theorem ex2 : foo.x = 0 :=
|
|
rfl
|
|
|
|
instance : HasEmptyc A :=
|
|
⟨{ x := 10 }⟩
|
|
|
|
def boo : A :=
|
|
{} -- this HasEmptyc.emptyc
|
|
|
|
theorem ex3 : boo.x = 10 :=
|
|
rfl
|