Instances For
def
Lean.Elab.Deriving.DecEq.mkMatch
(header : Lean.Elab.Deriving.Header)
(indVal : Lean.InductiveVal)
(auxFunName : Lake.Name)
:
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Lean.Elab.Deriving.DecEq.mkMatch.mkAlts
(indVal : Lean.InductiveVal)
(auxFunName : Lake.Name)
:
Lean.Elab.TermElabM (Array (Lean.TSyntax `Lean.Parser.Term.matchAlt))