## Stream: lean4

### Topic: simp instance trace

#### Sebastien Gouezel (Jan 29 2021 at 08:31):

I am trying to get the instance trace of simp calls in Lean4. In the following example, in mythm I get the trace of the first simp call (in A), but not of the second one (in B). Is there a way to access this trace in the current state of the Lean4 vscode extension, or should I just wait?

class MyClass (α : Type) where
foo1 : α
foo2 : α

class MyClass2 (α : Type) [MyClass α] where
foo_eq : (MyClass.foo1 : α) = MyClass.foo2

class MyClass3 (α : Type) [MyClass α] extends MyClass2 α

@[simp] theorem mysimp (α : Type) [MyClass α] [MyClass3 α] : (MyClass.foo1 : α) = MyClass.foo2 :=
MyClass2.foo_eq

set_option trace.Meta.synthInstance true

theorem mythm (α : Type) [MyClass α] [MyClass3 α] (x : α) : x = x := by
have A : (MyClass.foo1 : α) = MyClass.foo2 by simp
have B : (MyClass.foo1 : α) = MyClass.foo2 by simp
rfl


#### Sebastien Gouezel (Jan 29 2021 at 08:42):

It must be a caching mechanism: if I modify the example so that the second simp has to make a genuine new search, then I get the instance trace. So everything is fine!

Last updated: May 07 2021 at 13:21 UTC