Documentation
Lean
.
Elab
.
Deriving
.
Ord
Search
return to top
source
Imports
Lean.Meta.Transform
Lean.Elab.Deriving.Basic
Lean.Elab.Deriving.Util
Imported by
Lean
.
Elab
.
Deriving
.
Ord
.
mkOrdHeader
Lean
.
Elab
.
Deriving
.
Ord
.
mkMatch
Lean
.
Elab
.
Deriving
.
Ord
.
mkMatch
.
mkAlts
Lean
.
Elab
.
Deriving
.
Ord
.
mkAuxFunction
Lean
.
Elab
.
Deriving
.
Ord
.
mkMutualBlock
Lean
.
Elab
.
Deriving
.
Ord
.
mkOrdInstanceHandler
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkOrdHeader
(
indVal
:
InductiveVal
)
:
TermElabM
Header
Equations
Instances For
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkMatch
(
header
:
Header
)
(
indVal
:
InductiveVal
)
:
TermElabM
Term
Equations
Instances For
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkMatch
.
mkAlts
(
indVal
:
InductiveVal
)
:
TermElabM
(
Array
(
TSyntax
`Lean.Parser.Term.matchAlt
))
Equations
Instances For
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkAuxFunction
(
ctx
:
Context
)
(
i
:
Nat
)
:
TermElabM
Command
Equations
Instances For
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkMutualBlock
(
ctx
:
Context
)
:
TermElabM
Syntax
Equations
Instances For
source
def
Lean
.
Elab
.
Deriving
.
Ord
.
mkOrdInstanceHandler
(
declNames
:
Array
Name
)
:
Command.CommandElabM
Bool
Equations
Instances For