feat: add Meta.synthInstance.apply trace class (#12699)
This PR gives the `generate` function's "apply @Foo to Goal" trace nodes their own trace sub-class `Meta.synthInstance.apply` instead of sharing the parent `Meta.synthInstance` class. This allows metaprograms that walk synthesis traces to distinguish instance application attempts from other synthesis nodes by checking `td.cls` rather than string-matching on the header text. The new class is registered with `inherited := true`, so `set_option trace.Meta.synthInstance true` continues to show these nodes. Motivated by mathlib's `#defeq_abuse` diagnostic tactic (https://github.com/leanprover-community/mathlib4/pull/35750) which currently checks `headerStr.contains "apply"` to identify these nodes. See https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/backward.2EisDefEq.2ErespectTransparency 🤖 Prepared with Claude Code --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
This commit is contained in:
Kim Morrison
GitHub
parent
5dd8d570fd
commit
235b0eb987
7 changed files with 113 additions and 112 deletions
|
|
@ -573,7 +573,7 @@ def generate : SynthM Unit := do
|
|||
modify fun s => { s with generatorStack := s.generatorStack.pop }
|
||||
return
|
||||
discard do withMCtx mctx do
|
||||
withTraceNode `Meta.synthInstance
|
||||
withTraceNode `Meta.synthInstance.apply
|
||||
(return m!"{exceptOptionEmoji ·} apply {inst.val} to {← instantiateMVars (← inferType mvar)}") do
|
||||
modifyTop fun gNode => { gNode with currInstanceIdx := idx }
|
||||
if let some (mctx, subgoals) ← tryResolve mvar inst then
|
||||
|
|
@ -982,6 +982,7 @@ register_builtin_option trace.Meta.synthInstance : Bool := {
|
|||
|
||||
builtin_initialize
|
||||
registerTraceClass `Meta.synthPending
|
||||
registerTraceClass `Meta.synthInstance.apply (inherited := true)
|
||||
registerTraceClass `Meta.synthInstance.instances (inherited := true)
|
||||
registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
|
||||
registerTraceClass `Meta.synthInstance.answer (inherited := true)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
[Meta.synthInstance] ✅️ Inhabited Nat
|
||||
[Meta.synthInstance] new goal Inhabited Nat
|
||||
[Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
|
||||
[Meta.synthInstance] ✅️ apply instInhabitedNat to Inhabited Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply instInhabitedNat to Inhabited Nat
|
||||
[Meta.synthInstance.tryResolve] ✅️ Inhabited Nat ≟ Inhabited Nat
|
||||
[Meta.synthInstance.answer] ✅️ Inhabited Nat
|
||||
[Meta.synthInstance] result instInhabitedNat
|
||||
|
|
|
|||
|
|
@ -8,15 +8,15 @@
|
|||
[Meta.synthInstance] ✅️ IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g a => f (g a) d ≟ IsSmooth f
|
||||
[Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g a => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d
|
||||
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth f
|
||||
[Meta.synthInstance] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
|
||||
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
|
||||
has unused arguments, reduced type
|
||||
|
|
@ -25,7 +25,7 @@
|
|||
fun redf a => redf
|
||||
[Meta.synthInstance] new goal IsSmooth f
|
||||
[Meta.synthInstance.instances] #[inst✝]
|
||||
[Meta.synthInstance] ✅️ apply inst✝ to IsSmooth f
|
||||
[Meta.synthInstance.apply] ✅️ apply inst✝ to IsSmooth f
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth f ≟ IsSmooth f
|
||||
[Meta.synthInstance.answer] ✅️ IsSmooth f
|
||||
[Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
|
|
@ -45,23 +45,23 @@
|
|||
fun redf a => redf
|
||||
[Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b)
|
||||
[Meta.synthInstance.instances] #[inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (b : β), IsSmooth (f b)
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth (f b) ≟ IsSmooth f
|
||||
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
|
||||
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d
|
||||
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a) ≟ IsSmooth f
|
||||
[Meta.synthInstance] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.apply] ✅️ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1
|
||||
[Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f
|
||||
[Meta.synthInstance] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ✅️ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
|
||||
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a : δ), IsSmooth f
|
||||
has unused arguments, reduced type
|
||||
|
|
@ -76,23 +76,23 @@
|
|||
∀ (b : β), IsSmooth (f b)
|
||||
Transformer
|
||||
fun redf a a_1 => redf
|
||||
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1)
|
||||
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a
|
||||
[Meta.synthInstance.unusedArgs] ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a)
|
||||
has unused arguments, reduced type
|
||||
∀ (a : α), IsSmooth fun g => f (g a)
|
||||
Transformer
|
||||
fun redf a a_1 => redf a
|
||||
[Meta.synthInstance] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ❌️ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a
|
||||
[Meta.synthInstance] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.apply] ❌️ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a
|
||||
[Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g =>
|
||||
f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
|
||||
[Meta.synthInstance] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.apply] ✅️ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a)
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a)
|
||||
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth f
|
||||
has unused arguments, reduced type
|
||||
|
|
@ -104,13 +104,13 @@
|
|||
[Meta.synthInstance.resume] size: 1
|
||||
[Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth f
|
||||
[Meta.synthInstance] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.apply] ❌️ apply @diag to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1)
|
||||
[Meta.synthInstance] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.apply] ❌️ apply @comp to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1)
|
||||
[Meta.synthInstance] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.apply] ✅️ apply @parm to ∀ (a : α), IsSmooth fun g => g a
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a
|
||||
[Meta.synthInstance.unusedArgs] ∀ (a : α), IsSmooth fun g => g
|
||||
has unused arguments, reduced type
|
||||
|
|
@ -119,19 +119,19 @@
|
|||
fun redf a => redf
|
||||
[Meta.synthInstance] new goal IsSmooth fun g => g
|
||||
[Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝]
|
||||
[Meta.synthInstance] ❌️ apply inst✝ to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ❌️ apply inst✝ to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth f
|
||||
[Meta.synthInstance] ✅️ apply @swap to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ✅️ apply @swap to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun b a => b a
|
||||
[Meta.synthInstance] ❌️ apply @diag to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ❌️ apply @diag to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a)
|
||||
[Meta.synthInstance] ❌️ apply @comp to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ❌️ apply @comp to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a)
|
||||
[Meta.synthInstance] ❌️ apply @parm to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ❌️ apply @parm to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m
|
||||
[Meta.synthInstance] ❌️ apply @const to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ❌️ apply @const to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ❌️ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
|
||||
[Meta.synthInstance] ✅️ apply @identity to IsSmooth fun g => g
|
||||
[Meta.synthInstance.apply] ✅️ apply @identity to IsSmooth fun g => g
|
||||
[Meta.synthInstance.tryResolve] ✅️ IsSmooth fun g => g ≟ IsSmooth fun a => a
|
||||
[Meta.synthInstance.answer] ✅️ IsSmooth fun g => g
|
||||
[Meta.synthInstance.resume] propagating IsSmooth fun a =>
|
||||
|
|
|
|||
|
|
@ -17,51 +17,51 @@ info: B.foo "hello" : String × String
|
|||
trace: [Meta.synthInstance] ❌️ Add String
|
||||
[Meta.synthInstance] new goal Add String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
|
||||
[Meta.synthInstance] new goal Lean.Grind.Semiring String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
|
||||
[Meta.synthInstance] new goal Lean.Grind.CommSemiring String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring String ≟ Lean.Grind.CommSemiring String
|
||||
[Meta.synthInstance] new goal Lean.Grind.CommRing String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing String ≟ Lean.Grind.CommRing String
|
||||
[Meta.synthInstance] no instances for Lean.Grind.Field String
|
||||
[Meta.synthInstance.instances] #[]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring String ≟ Lean.Grind.Semiring String
|
||||
[Meta.synthInstance] new goal Lean.Grind.Ring String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring String ≟ Lean.Grind.Ring String
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Add String ≟ Add String
|
||||
[Meta.synthInstance] new goal Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance] new goal Lean.Grind.NatModule String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule String ≟ Lean.Grind.NatModule String
|
||||
[Meta.synthInstance] new goal Lean.Grind.IntModule String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule String ≟ Lean.Grind.IntModule String
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid String ≟ Lean.Grind.AddCommMonoid String
|
||||
[Meta.synthInstance] new goal Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup String ≟ Lean.Grind.AddCommGroup String
|
||||
[Meta.synthInstance] result <not-available>
|
||||
-/
|
||||
|
|
@ -74,51 +74,51 @@ trace: [Meta.synthInstance] ❌️ Add String
|
|||
trace: [Meta.synthInstance] ❌️ Add Bool
|
||||
[Meta.synthInstance] new goal Add Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommMonoid.toAdd, @Lean.Grind.Semiring.toAdd]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toAdd to Add Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toSemiring, @Lean.Grind.CommSemiring.toSemiring]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommSemiring.toSemiring to Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.CommSemiring Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toCommSemiring]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toCommSemiring to Lean.Grind.CommSemiring Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommSemiring Bool ≟ Lean.Grind.CommSemiring Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.CommRing Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Field.toCommRing]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Field.toCommRing to Lean.Grind.CommRing Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.CommRing Bool ≟ Lean.Grind.CommRing Bool
|
||||
[Meta.synthInstance] no instances for Lean.Grind.Field Bool
|
||||
[Meta.synthInstance.instances] #[]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toSemiring to Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Semiring Bool ≟ Lean.Grind.Semiring Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.Ring Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toRing]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.CommRing.toRing to Lean.Grind.Ring Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.Ring Bool ≟ Lean.Grind.Ring Bool
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommMonoid.toAdd to Add Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Add Bool ≟ Add Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.AddCommGroup.toAddCommMonoid, @Lean.Grind.NatModule.toAddCommMonoid]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.NatModule.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toNatModule, @Lean.Grind.Semiring.toNatModule]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Semiring.toNatModule to Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toNatModule to Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.NatModule Bool ≟ Lean.Grind.NatModule Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.IntModule Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Ring.toIntModule]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toIntModule to Lean.Grind.IntModule Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.IntModule Bool ≟ Lean.Grind.IntModule Bool
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.AddCommGroup.toAddCommMonoid to Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommMonoid Bool ≟ Lean.Grind.AddCommMonoid Bool
|
||||
[Meta.synthInstance] new goal Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.IntModule.toAddCommGroup, @Lean.Grind.Ring.toAddCommGroup]
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.Ring.toAddCommGroup to Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply @Lean.Grind.IntModule.toAddCommGroup to Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance.tryResolve] ✅️ Lean.Grind.AddCommGroup Bool ≟ Lean.Grind.AddCommGroup Bool
|
||||
[Meta.synthInstance] result <not-available>
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
[Meta.synthInstance] 💥️ OfNat ?m 1
|
||||
[Meta.synthInstance] new goal OfNat ?m 1
|
||||
[Meta.synthInstance.instances] #[@Lean.Grind.Semiring.ofNat, @One.toOfNat1, @Int16.instOfNat, @UInt64.instOfNat, @Rat.instOfNat, @Int8.instOfNat, @instOfNatFloat, @BitVec.instOfNat, Dyadic.instOfNat, @Int64.instOfNat, @instOfNat, @Id.instOfNat, @UInt16.instOfNat, instOfNatNat, @UInt32.instOfNat, @UInt8.instOfNat, @Fin.instOfNat, @ISize.instOfNat, @instOfNatFloat32, @Int32.instOfNat, @USize.instOfNat]
|
||||
[Meta.synthInstance] 💥️ apply @USize.instOfNat to OfNat ?m 1
|
||||
[Meta.synthInstance.apply] 💥️ apply @USize.instOfNat to OfNat ?m 1
|
||||
[Meta.synthInstance.tryResolve] 💥️ OfNat ?m 1 ≟ OfNat USize ?m
|
||||
[Meta.Tactic.simp.rewrite] Nat.add_succ:1000:
|
||||
x + 1
|
||||
|
|
|
|||
|
|
@ -1,11 +1,11 @@
|
|||
[Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
|
||||
[Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
|
||||
|
|
@ -14,15 +14,15 @@
|
|||
[Meta.synthInstance.resume] size: 1
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
(ReaderT Elab.Term.Context
|
||||
|
|
@ -37,16 +37,16 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.resume] propagating MonadLift MetaM
|
||||
|
|
@ -64,7 +64,7 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.resume] propagating MonadEvalT MetaM
|
||||
MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
|
|
@ -84,16 +84,16 @@
|
|||
[Meta.synthInstance] ✅️ HasCoerce Nat Prop
|
||||
[Meta.synthInstance] new goal HasCoerce Nat Prop
|
||||
[Meta.synthInstance.instances] #[@coerceTrans]
|
||||
[Meta.synthInstance] ✅️ apply @coerceTrans to HasCoerce Nat Prop
|
||||
[Meta.synthInstance.apply] ✅️ apply @coerceTrans to HasCoerce Nat Prop
|
||||
[Meta.synthInstance] new goal HasCoerce _tc.0 Prop
|
||||
[Meta.synthInstance.instances] #[@coerceTrans, coerceBoolToProp]
|
||||
[Meta.synthInstance] ✅️ apply coerceBoolToProp to HasCoerce Bool Prop
|
||||
[Meta.synthInstance.apply] ✅️ apply coerceBoolToProp to HasCoerce Bool Prop
|
||||
[Meta.synthInstance.answer] ✅️ HasCoerce Bool Prop
|
||||
[Meta.synthInstance.resume] propagating HasCoerce Bool Prop to subgoal HasCoerce Bool Prop of HasCoerce Nat Prop
|
||||
[Meta.synthInstance.resume] size: 1
|
||||
[Meta.synthInstance] new goal HasCoerce Nat Bool
|
||||
[Meta.synthInstance.instances] #[@coerceTrans, coerceNatToBool]
|
||||
[Meta.synthInstance] ✅️ apply coerceNatToBool to HasCoerce Nat Bool
|
||||
[Meta.synthInstance.apply] ✅️ apply coerceNatToBool to HasCoerce Nat Bool
|
||||
[Meta.synthInstance.answer] ✅️ HasCoerce Nat Bool
|
||||
[Meta.synthInstance.resume] propagating HasCoerce Nat Bool to subgoal HasCoerce Nat Bool of HasCoerce Nat Prop
|
||||
[Meta.synthInstance.resume] size: 2
|
||||
|
|
@ -103,11 +103,11 @@
|
|||
[Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
|
||||
[Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
|
||||
|
|
@ -116,15 +116,15 @@
|
|||
[Meta.synthInstance.resume] size: 1
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
(ReaderT Elab.Term.Context
|
||||
|
|
@ -139,16 +139,16 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.resume] propagating MonadLift MetaM
|
||||
|
|
@ -166,7 +166,7 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.resume] propagating MonadEvalT MetaM
|
||||
MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
|
|
@ -186,10 +186,10 @@
|
|||
[Meta.synthInstance] ✅️ Bind IO
|
||||
[Meta.synthInstance] new goal Bind IO
|
||||
[Meta.synthInstance.instances] #[@Monad.toBind]
|
||||
[Meta.synthInstance] ✅️ apply @Monad.toBind to Bind IO
|
||||
[Meta.synthInstance.apply] ✅️ apply @Monad.toBind to Bind IO
|
||||
[Meta.synthInstance] new goal Monad IO
|
||||
[Meta.synthInstance.instances] #[@instMonadEIO]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEIO to Monad IO
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEIO to Monad IO
|
||||
[Meta.synthInstance.answer] ✅️ Monad IO
|
||||
[Meta.synthInstance.resume] propagating Monad (EIO IO.Error) to subgoal Monad IO of Bind IO
|
||||
[Meta.synthInstance.resume] size: 1
|
||||
|
|
@ -199,11 +199,11 @@
|
|||
[Meta.synthInstance] ✅️ MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift, Elab.Command.instMonadEvalTermElabMCommandElabM]
|
||||
[Meta.synthInstance] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply Elab.Command.instMonadEvalTermElabMCommandElabM to MonadEval Elab.TermElabM
|
||||
Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEval Elab.TermElabM Elab.Command.CommandElabM
|
||||
[Meta.synthInstance.resume] propagating MonadEval Elab.TermElabM
|
||||
|
|
@ -212,15 +212,15 @@
|
|||
[Meta.synthInstance.resume] size: 1
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m Elab.TermElabM
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 Elab.TermElabM
|
||||
[Meta.synthInstance.instances] #[@ReaderT.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @ReaderT.instMonadLift to MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
Elab.TermElabM
|
||||
[Meta.synthInstance.apply] ✅️ apply @ReaderT.instMonadLift to MonadLift
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM) Elab.TermElabM
|
||||
[Meta.synthInstance.resume] propagating MonadLift (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
(ReaderT Elab.Term.Context
|
||||
|
|
@ -235,16 +235,16 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
[Meta.synthInstance.apply] ❌️ apply instMonadEvalT to MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalTOfMonadEval to MonadEvalT MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadEval _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@instMonadEvalOfMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
[Meta.synthInstance.apply] ✅️ apply @instMonadEvalOfMonadLift to MonadEval ?m
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance] new goal MonadLift _tc.1 (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.instances] #[@StateRefT'.instMonadLift]
|
||||
[Meta.synthInstance] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply @StateRefT'.instMonadLift to MonadLift MetaM
|
||||
(StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.answer] ✅️ MonadLift MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
[Meta.synthInstance.resume] propagating MonadLift MetaM
|
||||
|
|
@ -262,7 +262,7 @@
|
|||
[Meta.synthInstance.resume] size: 2
|
||||
[Meta.synthInstance] new goal MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.instances] #[instMonadEvalTOfMonadEval, instMonadEvalT]
|
||||
[Meta.synthInstance] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.apply] ✅️ apply instMonadEvalT to MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.answer] ✅️ MonadEvalT MetaM MetaM
|
||||
[Meta.synthInstance.resume] propagating MonadEvalT MetaM
|
||||
MetaM to subgoal MonadEvalT MetaM MetaM of MonadEvalT MetaM (StateRefT' IO.RealWorld Elab.Term.State MetaM)
|
||||
|
|
@ -282,25 +282,25 @@
|
|||
[Meta.synthInstance] ✅️ BEq Nat
|
||||
[Meta.synthInstance] new goal BEq Nat
|
||||
[Meta.synthInstance.instances] #[@instBEqOfDecidableEq, @Std.PreorderPackage.toBEq]
|
||||
[Meta.synthInstance] ✅️ apply @Std.PreorderPackage.toBEq to BEq Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @Std.PreorderPackage.toBEq to BEq Nat
|
||||
[Meta.synthInstance] new goal Std.PreorderPackage Nat
|
||||
[Meta.synthInstance.instances] #[@Std.PartialOrderPackage.toPreorderPackage, @Std.LinearPreorderPackage.toPreorderPackage]
|
||||
[Meta.synthInstance] ✅️ apply @Std.LinearPreorderPackage.toPreorderPackage to Std.PreorderPackage Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @Std.LinearPreorderPackage.toPreorderPackage to Std.PreorderPackage Nat
|
||||
[Meta.synthInstance] new goal Std.LinearPreorderPackage Nat
|
||||
[Meta.synthInstance.instances] #[@Std.LinearOrderPackage.toLinearPreorderPackage]
|
||||
[Meta.synthInstance] ✅️ apply @Std.LinearOrderPackage.toLinearPreorderPackage to Std.LinearPreorderPackage Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @Std.LinearOrderPackage.toLinearPreorderPackage to Std.LinearPreorderPackage Nat
|
||||
[Meta.synthInstance] no instances for Std.LinearOrderPackage Nat
|
||||
[Meta.synthInstance.instances] #[]
|
||||
[Meta.synthInstance] ✅️ apply @Std.PartialOrderPackage.toPreorderPackage to Std.PreorderPackage Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @Std.PartialOrderPackage.toPreorderPackage to Std.PreorderPackage Nat
|
||||
[Meta.synthInstance] new goal Std.PartialOrderPackage Nat
|
||||
[Meta.synthInstance.instances] #[@Std.LinearOrderPackage.toPartialOrderPackage]
|
||||
[Meta.synthInstance] ✅️ apply @Std.LinearOrderPackage.toPartialOrderPackage to Std.PartialOrderPackage Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @Std.LinearOrderPackage.toPartialOrderPackage to Std.PartialOrderPackage Nat
|
||||
[Meta.synthInstance] no instances for Std.LinearOrderPackage Nat
|
||||
[Meta.synthInstance.instances] #[]
|
||||
[Meta.synthInstance] ✅️ apply @instBEqOfDecidableEq to BEq Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply @instBEqOfDecidableEq to BEq Nat
|
||||
[Meta.synthInstance] new goal DecidableEq Nat
|
||||
[Meta.synthInstance.instances] #[instDecidableEqNat]
|
||||
[Meta.synthInstance] ✅️ apply instDecidableEqNat to DecidableEq Nat
|
||||
[Meta.synthInstance.apply] ✅️ apply instDecidableEqNat to DecidableEq Nat
|
||||
[Meta.synthInstance.answer] ✅️ DecidableEq Nat
|
||||
[Meta.synthInstance.resume] propagating DecidableEq Nat to subgoal DecidableEq Nat of BEq Nat
|
||||
[Meta.synthInstance.resume] size: 1
|
||||
|
|
|
|||
|
|
@ -24,7 +24,7 @@ error: failed to synthesize instance of type class
|
|||
trace: [Meta.synthInstance] ❌️ Foo "two"
|
||||
[Meta.synthInstance] new goal Foo "two"
|
||||
[Meta.synthInstance.instances] #[@instFoo_1]
|
||||
[Meta.synthInstance] ✅️ apply @instFoo_1 to Foo "two"
|
||||
[Meta.synthInstance.apply] ✅️ apply @instFoo_1 to Foo "two"
|
||||
[Meta.synthInstance.tryResolve] ✅️ Foo "two" ≟ Foo "two"
|
||||
[Meta.synthInstance] no instances for Foo "three"
|
||||
[Meta.synthInstance.instances] #[]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue