Documentation

Lean.Elab.Deriving.Inhabited

source
def Lean.Elab.mkInhabitedInstanceHandler (declNames : Array Lean.Name) :
Lean.Elab.Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.