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