max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test: copyNewFieldsFrom

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-10 09:19:27 -07:00
parent 50deae9b8b
commit d03fa17c49
2 changed files with 42 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
tests/lean/diamond6.lean
View file

@ -17,3 +17,19 @@ set_option pp.all true
#check @FooAC.mk
#print FooAC.toFooAssoc
class FooAssoc' (α : Type) extends FooAssoc α where
one : α
class FooAC' (α : Type) extends FooComm α, FooAssoc' α where
mul_comm (a b : α) : a * b = b * a
#check @FooAC'.mk
#print FooAC'.toFooAssoc'
def f [FooAssoc α] (a : α) : α :=
a * a
def g [FooAC' α] (a : α) : α :=
f (a + FooAssoc'.one)

26
tests/lean/diamond6.lean.expected.out
View file

@ -21,3 +21,29 @@ def FooAC.toFooAssoc : {α : Type} → [self : FooAC α] → FooAssoc α :=
fun (α : Type) [self : FooAC α] =>
@FooAssoc.mk α (@FooComm.toFoo α (@FooAC.toFooComm α self)) (@FooAC.toMul α self) (@FooAC.add_assoc α self)
(@FooAC.mul_assoc α self)
@FooAC'.mk : {α : Type} →
[toFooComm : FooComm α] →
[toMul : Mul.{0} α] →
(∀ (a b c : α),
@Eq.{1} α
(@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm)))
(@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a b) c)
(@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) a
(@HAdd.hAdd.{0, 0, 0} α α α (@instHAdd.{0} α (@Foo.toAdd α (@FooComm.toFoo α toFooComm))) b c))) →
(∀ (a b c : α),
@Eq.{1} α
(@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul)
(@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b) c)
(@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a
(@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b c))) →
α →
(∀ (a b : α),
@Eq.{1} α (@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) a b)
(@HMul.hMul.{0, 0, 0} α α α (@instHMul.{0} α toMul) b a)) →
FooAC' α
def FooAC'.toFooAssoc' : {α : Type} → [self : FooAC' α] → FooAssoc' α :=
fun (α : Type) [self : FooAC' α] =>
@FooAssoc'.mk α
(@FooAssoc.mk α (@FooComm.toFoo α (@FooAC'.toFooComm α self)) (@FooAC'.toMul α self) (@FooAC'.add_assoc α self)
(@FooAC'.mul_assoc α self))
(@FooAC'.one α self)