feat: add basic isDefEq cache
This commit is contained in:
Leonardo de Moura
parent
51e03837f5
commit
49a87ceb4d
5 changed files with 223 additions and 38 deletions
|
|
@ -98,12 +98,19 @@ abbrev SynthInstanceCache := PersistentHashMap Expr (Option Expr)
|
|||
abbrev InferTypeCache := PersistentExprStructMap Expr
|
||||
abbrev FunInfoCache := PersistentHashMap InfoCacheKey FunInfo
|
||||
abbrev WhnfCache := PersistentExprStructMap Expr
|
||||
|
||||
/- A set of pairs. TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
|
||||
We should also investigate the impact on memory consumption. -/
|
||||
abbrev DefEqCache := PersistentHashMap (Expr × Expr) Unit
|
||||
|
||||
structure Cache where
|
||||
inferType : InferTypeCache := {}
|
||||
funInfo : FunInfoCache := {}
|
||||
synthInstance : SynthInstanceCache := {}
|
||||
whnfDefault : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
|
||||
whnfAll : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
|
||||
defEqDefault : DefEqCache := {}
|
||||
defEqAll : DefEqCache := {}
|
||||
deriving Inhabited
|
||||
|
||||
/--
|
||||
|
|
@ -218,7 +225,7 @@ variable [MonadControlT MetaM n] [Monad n]
|
|||
modify fun ⟨mctx, cache, zetaFVarIds, postponed⟩ => ⟨mctx, f cache, zetaFVarIds, postponed⟩
|
||||
|
||||
@[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
|
||||
modifyCache fun ⟨ic, c1, c2, c3, c4⟩ => ⟨f ic, c1, c2, c3, c4⟩
|
||||
modifyCache fun ⟨ic, c1, c2, c3, c4, c5, c6⟩ => ⟨f ic, c1, c2, c3, c4, c5, c6⟩
|
||||
|
||||
def getLocalInstances : MetaM LocalInstances :=
|
||||
return (← read).localInstances
|
||||
|
|
|
|||
|
|
@ -999,8 +999,6 @@ private def tryHeuristic (t s : Expr) : MetaM Bool := do
|
|||
when `t` and `s` do not have metavariables, are not structurally equal, and `f` is an abbreviation.
|
||||
On the other hand, by unfolding `f`, we often produce smaller terms. -/
|
||||
unless info.hints.isRegular do
|
||||
t ← instantiateMVars t
|
||||
s ← instantiateMVars s
|
||||
unless t.hasExprMVar || s.hasExprMVar do
|
||||
return false
|
||||
traceCtx `Meta.isDefEq.delta do
|
||||
|
|
@ -1405,6 +1403,43 @@ private def isDefEqApp (t s : Expr) : MetaM Bool := do
|
|||
else
|
||||
isDefEqOnFailure t s
|
||||
|
||||
private def isExprDefEqExpensive (t : Expr) (s : Expr) : MetaM Bool := do
|
||||
if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else
|
||||
if (← isDefEqProj t s) then pure true else
|
||||
whenUndefDo (isDefEqNative t s) do
|
||||
whenUndefDo (isDefEqNat t s) do
|
||||
whenUndefDo (isDefEqOffset t s) do
|
||||
whenUndefDo (isDefEqDelta t s) do
|
||||
if t.isConst && s.isConst then
|
||||
if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else pure false
|
||||
else if t.isApp && s.isApp then
|
||||
isDefEqApp t s
|
||||
else
|
||||
whenUndefDo (isDefEqStringLit t s) do
|
||||
isDefEqOnFailure t s
|
||||
|
||||
-- We only check DefEq cache for default and all transparency modes
|
||||
private def skipDefEqCache : MetaM Bool := do
|
||||
match (← getConfig).transparency with
|
||||
| TransparencyMode.default => return false
|
||||
| TransparencyMode.all => return false
|
||||
| _ => return true
|
||||
|
||||
private def mkCacheKey (t : Expr) (s : Expr) : Expr × Expr :=
|
||||
if Expr.quickLt t s then (t, s) else (s, t)
|
||||
|
||||
private def isCached (key : Expr × Expr) : MetaM Bool := do
|
||||
match (← getConfig).transparency with
|
||||
| TransparencyMode.default => return (← get).cache.defEqDefault.contains key
|
||||
| TransparencyMode.all => return (← get).cache.defEqAll.contains key
|
||||
| _ => return false
|
||||
|
||||
private def cacheResult (key : Expr × Expr) : MetaM Unit := do
|
||||
match (← getConfig).transparency with
|
||||
| TransparencyMode.default => modify fun s => { s with cache.defEqDefault := s.cache.defEqDefault.insert key () }
|
||||
| TransparencyMode.all => modify fun s => { s with cache.defEqAll := s.cache.defEqAll.insert key () }
|
||||
| _ => pure ()
|
||||
|
||||
partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do
|
||||
trace[Meta.isDefEq.step] "{t} =?= {s}"
|
||||
checkMaxHeartbeats "isDefEq"
|
||||
|
|
@ -1415,20 +1450,31 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := do
|
|||
let s' ← whnfCore s
|
||||
if t != t' || s != s' then
|
||||
isExprDefEqAuxImpl t' s'
|
||||
else do
|
||||
if (← (isDefEqEta t s <||> isDefEqEta s t)) then pure true else
|
||||
if (← isDefEqProj t s) then pure true else
|
||||
whenUndefDo (isDefEqNative t s) do
|
||||
whenUndefDo (isDefEqNat t s) do
|
||||
whenUndefDo (isDefEqOffset t s) do
|
||||
whenUndefDo (isDefEqDelta t s) do
|
||||
if t.isConst && s.isConst then
|
||||
if t.constName! == s.constName! then isListLevelDefEqAux t.constLevels! s.constLevels! else pure false
|
||||
else if t.isApp && s.isApp then
|
||||
isDefEqApp t s
|
||||
else if (← skipDefEqCache) then
|
||||
isExprDefEqExpensive t s
|
||||
else
|
||||
/-
|
||||
TODO: check whether the following `instantiateMVar`s are expensive or not in practice.
|
||||
Lean 3 does not use them, and may miss caching opportunities since it is not safe to cache when `t` and `s` may contain mvars.
|
||||
The unit test `tryHeuristicPerfIssue2.lean` cannot be solved without these two `instantiateMVar`s.
|
||||
If it becomes a problem, we may use store a flag in the context indicating whether we have already used `instantiateMVar` in
|
||||
outer invocations or not. It is not perfect (we may assign mvars in nested calls), but it should work well enough in practice,
|
||||
and prevent repeated traversals in nested calls.
|
||||
-/
|
||||
let t ← instantiateMVars t
|
||||
let s ← instantiateMVars s
|
||||
if t.hasMVar || s.hasMVar then
|
||||
-- It is not safe to use DefEq cache if terms contain metavariables
|
||||
isExprDefEqExpensive t s
|
||||
else
|
||||
whenUndefDo (isDefEqStringLit t s) do
|
||||
isDefEqOnFailure t s
|
||||
let k := mkCacheKey t s
|
||||
if (← isCached k) then
|
||||
return true
|
||||
else if (← isExprDefEqExpensive t s) then
|
||||
cacheResult k
|
||||
return true
|
||||
else
|
||||
return false
|
||||
|
||||
builtin_initialize
|
||||
isExprDefEqAuxRef.set isExprDefEqAuxImpl
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
[Elab.info] command @ ⟨13, 0⟩-⟨15, 6⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.534} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
[.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
|
||||
x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
|
||||
Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩ @ myMacro._@.Init.Notation._hyg.2258
|
||||
|
|
@ -11,10 +11,10 @@
|
|||
Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩ @ Lean.Elab.Term.elabApp
|
||||
Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 27⟩†
|
||||
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.538} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
[.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.537} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
[.] `Nat : some Type.{?_uniq.538} @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
Nat : Type @ ⟨13, 24⟩-⟨13, 27⟩
|
||||
let y : Nat × Nat := (x, x);
|
||||
id y : Nat × Nat @ ⟨14, 2⟩-⟨15, 6⟩ @ Lean.Elab.Term.elabLetDecl
|
||||
|
|
@ -39,16 +39,16 @@
|
|||
[Elab.info] command @ ⟨17, 0⟩-⟨19, 8⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
∀ (x y : Nat), Bool → x + 0 = x : Prop @ ⟨17, 8⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.567} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.566} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
x : Nat @ ⟨17, 9⟩-⟨17, 10⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.569} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
[.] `Nat : some Sort.{?_uniq.568} @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
Nat : Type @ ⟨17, 15⟩-⟨17, 18⟩
|
||||
y : Nat @ ⟨17, 11⟩-⟨17, 12⟩
|
||||
Bool → x + 0 = x : Prop @ ⟨17, 22⟩-⟨17, 44⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Bool : some Sort.{?_uniq.572} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
[.] `Bool : some Sort.{?_uniq.571} @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
|
||||
b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
|
||||
x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩ @ myMacro._@.Init.Notation._hyg.9563
|
||||
|
|
@ -115,20 +115,20 @@
|
|||
[Elab.info] command @ ⟨21, 0⟩-⟨25, 10⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat → Nat → Bool → Nat : Type @ ⟨21, 9⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.880} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.865} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
x : Nat @ ⟨21, 10⟩-⟨21, 11⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.882} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
[.] `Nat : some Sort.{?_uniq.867} @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
Nat : Type @ ⟨21, 16⟩-⟨21, 19⟩
|
||||
y : Nat @ ⟨21, 12⟩-⟨21, 13⟩
|
||||
Bool → Nat : Type @ ⟨21, 23⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabDepArrow
|
||||
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Bool : some Sort.{?_uniq.885} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
[.] `Bool : some Sort.{?_uniq.870} @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
Bool : Type @ ⟨21, 28⟩-⟨21, 32⟩
|
||||
b : Bool @ ⟨21, 24⟩-⟨21, 25⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.887} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
[.] `Nat : some Sort.{?_uniq.872} @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
Nat : Type @ ⟨21, 36⟩-⟨21, 39⟩
|
||||
fun (x y : Nat) (b : Bool) =>
|
||||
let x : Nat × Nat := (x + y, x - y);
|
||||
|
|
@ -239,10 +239,10 @@
|
|||
Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
|
||||
Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 35⟩†
|
||||
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.1890} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
[.] `Nat : some Type.{?_uniq.1827} @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
|
||||
Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.1889} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
[.] `Array : some Type.{?_uniq.1826} @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
|
||||
Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩ @ Lean.Elab.Term.expandParen
|
||||
Macro expansion
|
||||
|
|
@ -250,17 +250,17 @@
|
|||
===>
|
||||
Array Nat
|
||||
Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Type.{?_uniq.1891} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
[.] `Array : some Type.{?_uniq.1828} @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
|
||||
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.1892} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
[.] `Nat : some Type.{?_uniq.1829} @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
|
||||
s : Nat × Array (Array Nat) @ ⟨27, 8⟩-⟨27, 9⟩
|
||||
Array Nat : Type @ ⟨27, 39⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabApp
|
||||
[.] `Array : some Sort.{?_uniq.1894} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
[.] `Array : some Sort.{?_uniq.1831} @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
Array : Type → Type @ ⟨27, 39⟩-⟨27, 44⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Type.{?_uniq.1895} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
[.] `Nat : some Type.{?_uniq.1832} @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Nat : Type @ ⟨27, 45⟩-⟨27, 48⟩
|
||||
Array.push (Array.getOp s.snd 1) s.fst : Array Nat @ ⟨28, 2⟩-⟨28, 17⟩ @ Lean.Elab.Term.elabApp
|
||||
s : Nat × Array (Array Nat) @ ⟨28, 2⟩-⟨28, 3⟩
|
||||
|
|
@ -274,11 +274,11 @@
|
|||
Prod.fst : {α β : Type} → α × β → α @ ⟨28, 16⟩-⟨28, 17⟩
|
||||
[Elab.info] command @ ⟨30, 0⟩-⟨31, 20⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
B : Type @ ⟨30, 14⟩-⟨30, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.1936} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
[.] `B : some Sort.{?_uniq.1872} @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
B : Type @ ⟨30, 14⟩-⟨30, 15⟩
|
||||
arg : B @ ⟨30, 8⟩-⟨30, 11⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.1938} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
[.] `Nat : some Sort.{?_uniq.1874} @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
Nat : Type @ ⟨30, 19⟩-⟨30, 22⟩
|
||||
A.val arg.pair.fst 0 : Nat @ ⟨31, 2⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabApp
|
||||
arg : B @ ⟨31, 2⟩-⟨31, 5⟩
|
||||
|
|
@ -291,11 +291,11 @@
|
|||
0 : Nat @ ⟨31, 19⟩-⟨31, 20⟩ @ Lean.Elab.Term.elabNumLit
|
||||
[Elab.info] command @ ⟨33, 0⟩-⟨35, 1⟩ @ Lean.Elab.Command.elabDeclaration
|
||||
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `Nat : some Sort.{?_uniq.1958} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
[.] `Nat : some Sort.{?_uniq.1894} @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
Nat : Type @ ⟨33, 12⟩-⟨33, 15⟩
|
||||
x : Nat @ ⟨33, 8⟩-⟨33, 9⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩ @ Lean.Elab.Term.elabIdent
|
||||
[.] `B : some Sort.{?_uniq.1960} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
[.] `B : some Sort.{?_uniq.1896} @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
B : Type @ ⟨33, 19⟩-⟨33, 20⟩
|
||||
{ pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩ @ Lean.Elab.Term.StructInst.elabStructInst
|
||||
({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩ @ Lean.Elab.Term.expandParen
|
||||
|
|
|
|||
|
|
@ -100,8 +100,6 @@ class T1 (α : Type u) where
|
|||
addc8 : ∀ (x y : α), @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x
|
||||
addc9 : ∀ (x y : α), @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @Add.add α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x
|
||||
|
||||
set_option maxHeartbeats 10000000
|
||||
|
||||
-- slow
|
||||
instance T1.toL9 [inst : T1 α] : L9 α := { inst with }
|
||||
|
||||
|
|
|
|||
134
tests/lean/run/tryHeuristicPerfIssue2.lean
Normal file
134
tests/lean/run/tryHeuristicPerfIssue2.lean
Normal file
|
|
@ -0,0 +1,134 @@
|
|||
def myAdd [Add α] (x y : α) := x + y
|
||||
|
||||
class L1 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
|
||||
instance L1.toAdd [inst : L1 α] : Add α := { inst with }
|
||||
|
||||
class L2 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
|
||||
instance L2.toL1 [inst : L2 α] : L1 α := { inst with }
|
||||
|
||||
class L3 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
|
||||
instance L3.toL2 [inst : L3 α] : L2 α := { inst with }
|
||||
|
||||
class L4 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
|
||||
instance L4.toL3 [inst : L4 α] : L3 α := { inst with }
|
||||
|
||||
class L5 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
|
||||
instance L5.toL4 [inst : L5 α] : L4 α := { inst with }
|
||||
|
||||
class L6 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
|
||||
instance L6.toL5 [inst : L6 α] : L5 α := { inst with }
|
||||
|
||||
class L7 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x
|
||||
|
||||
instance L7.toL6 [inst : L7 α] : L6 α := { inst with }
|
||||
|
||||
class L8 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x
|
||||
addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x
|
||||
|
||||
instance L8.toL7 [inst : L8 α] : L7 α := { inst with }
|
||||
|
||||
class L9 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x
|
||||
addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x
|
||||
addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x
|
||||
|
||||
instance L9.toL8 [inst : L9 α] : L8 α := { inst with }
|
||||
|
||||
class T1 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x
|
||||
addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x
|
||||
addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x
|
||||
|
||||
-- slow
|
||||
instance T1_toL9 {α : Type u} [inst : T1 α] : L9 α := { inst with }
|
||||
|
||||
class T2 (α : Type u) where
|
||||
add : α → α → α
|
||||
addc1 : ∀ (x y : α), @myAdd α ⟨add⟩ x y = @myAdd α ⟨add⟩ y x
|
||||
addc2 : ∀ (x y : α), @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) x y = @myAdd α (@L1.toAdd _ ⟨add, addc1⟩) y x
|
||||
addc3 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ ⟨add, addc1, addc2⟩)) y x
|
||||
addc4 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ ⟨add, addc1, addc2, addc3⟩))) y x
|
||||
addc5 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ ⟨add, addc1, addc2, addc3, addc4⟩)))) y x
|
||||
addc6 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ ⟨add, addc1, addc2, addc3, addc4, addc5⟩))))) y x
|
||||
addc7 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6⟩)))))) y x
|
||||
addc8 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7⟩))))))) y x
|
||||
addc9 : ∀ (x y : α), @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) x y = @myAdd α (@L1.toAdd _ (@L2.toL1 _ (@L3.toL2 _ (@L4.toL3 _ (@L5.toL4 _ (@L6.toL5 _ (@L7.toL6 _ (@L8.toL7 _ ⟨add, addc1, addc2, addc3, addc4, addc5, addc6, addc7, addc8⟩)))))))) y x
|
||||
|
||||
-- slow
|
||||
instance T2_toL9 {α : Type u} [inst : T2 α] : L9 α := { inst with }
|
||||
|
||||
|
||||
set_option pp.all true in
|
||||
-- #print T2.toL9
|
||||
|
||||
axiom C : Type
|
||||
axiom C.add : C → C → C
|
||||
|
||||
noncomputable instance C.T1 : T1 C := ⟨add, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩
|
||||
noncomputable instance C.T2 : T2 C := ⟨add, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry, sorry⟩
|
||||
|
||||
-- slow
|
||||
theorem ex : @T1_toL9 _ C.T1 = @T2_toL9 _ C.T2 := rfl
|
||||
Loading…
Add table
Reference in a new issue