sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: add Meta.synthInstance.apply trace class (#12699)

Browse Source 
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
2026-03-01 18:06:56 +11:00
committed by Kim Morrison
parent 04d3ba35de
commit 0bbadfa02a
5 changed files with 60 additions and 59 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
src/Lean/Meta/SynthInstance.lean
View File

@@ -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)

2
tests/lean/366.lean.expected.out
View File

@@ -2,7 +2,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

58
tests/lean/815b.lean.expected.out
View File

@@ -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 =>

56
tests/lean/run/infoFromFailure.lean
View File

@@ -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>
-/

2
tests/lean/run/trace_synth.lean
View File

@@ -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] #[]