inferInstance Decidable for defs

Stream: new members

[Mark Aagaard]

The Lean4 type classes documentation says, "Sometimes Lean can't find an instance because the class is buried under a definition". So, I have:

def p1 (b:Bool) := b = true
-- doesn't work: deriving Decidable

instance (b:Bool) : Decidable (p1 b) :=
  inferInstanceAs (Decidable (b = true))

Is this the preferred method for showing decidability of p1? I'm curious if there is a tactic based approach where I could tell Lean to "unfold the definition of p1" rather than explicitly provide the body of p1.

-mark

[Eric Wieser]

Yes, the spelling you're asking for is by unfold p1; infer_instance

[Mark Aagaard]

@Eric Wieser - thanks!
-mark