Documentation

Lean.Elab.Deriving.Ord

source
def Lean.Elab.Deriving.Ord.mkOrdHeader (indVal : InductiveVal) :
TermElabM Header
Equations
source
def Lean.Elab.Deriving.Ord.mkMatch (header : Header) (indVal : InductiveVal) :
TermElabM Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Ord.mkMatch.mkAlts (indVal : InductiveVal) :
TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Ord.mkAuxFunction (ctx : Context) (i : Nat) :
TermElabM Command
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Ord.mkMutualBlock (ctx : Context) :
TermElabM Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Ord.mkOrdInstanceHandler (declNames : Array Name) :
Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.