Instances For
def
Lean.Elab.Deriving.Ord.mkMatch
(header : Lean.Elab.Deriving.Header)
(indVal : Lean.InductiveVal)
:
Instances For
def
Lean.Elab.Deriving.Ord.mkMatch.mkAlts
(indVal : Lean.InductiveVal)
:
Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))