Documentation

Lean.Elab.Deriving.Nonempty

source
def Lean.Elab.mkNonemptyInstanceHandler (declNames : Array Lake.Name) :
Lean.Elab.Command.CommandElabM Bool
Instances For