def Lean.Elab.Deriving.Hashable.mkHashableHeader (indVal : InductiveVal) : TermElabM Header

Equations

• Lean.Elab.Deriving.Hashable.mkHashableHeader indVal = Lean.Elab.Deriving.mkHeader `Hashable 1 indVal

def Lean.Elab.Deriving.Hashable.mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Term

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.Hashable.mkMatch.mkAlts (ctx : Context) (indVal : InductiveVal) : TermElabM (Array (TSyntax `Lean.Parser.Term.matchAlt))

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.Hashable.mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.Hashable.mkHashFuncs (ctx : Context) : TermElabM Syntax

Equations

• One or more equations did not get rendered due to their size.

def Lean.Elab.Deriving.Hashable.mkHashableHandler (declNames : Array Name) : Command.CommandElabM Bool

Equations

• One or more equations did not get rendered due to their size.