Documentation

Lean.Elab.Deriving.Inhabited

def Lean.Elab.mkInhabitedInstanceHandler (declNames : Array Lean.Name) :

Lean.Elab.Command.CommandElabM Bool

Equations

Lean.Elab.mkInhabitedInstanceHandler declNames = do let a ← Array.allM Lean.isInductive declNames 0 (Array.size declNames) if a = true then do Array.forM Lean.Elab.mkInhabitedInstance declNames 0 (Array.size declNames) pure true else pure false