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