Unfolding derived instances with simp

Stream: lean4

[Yann Herklotz]

I had maybe a naive question on how to make derived instances reducible, or add the instance to the simp set so that it is unfolded automatically? In the following example, we need to add BEq.beq, decide, instDecidableEqString, String.decEq manually to the simp set.

import Lean

def Ident' := String
deriving instance BEq for Ident'

example : (@Lean.AssocList.find? Ident' _ _ "a" (.cons "a" 0 .nil)) = some 0 := by
  dsimp [Lean.AssocList.find?, BEq.beq, decide, instDecidableEqString, String.decEq]

Instead, if one is using more primitive types, then dsimp works well without having to manually specify the instances above.

example : (@Lean.AssocList.find? String _ _ "a" (.cons "a" 0 .nil)) = some 0 := by
  dsimp [Lean.AssocList.find?]