Documentation

Lean.Elab.Deriving.BEq

source
def Lean.Elab.Deriving.BEq.mkBEqHeader (indVal : InductiveVal) :
TermElabM Header
Equations
source
def Lean.Elab.Deriving.BEq.mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) :
TermElabM Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.BEq.mkMatch.mkElseAlt (indVal : InductiveVal) :
TermElabM (TSyntax `Lean.Parser.Term.matchAltExpr)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.BEq.mkMatch.mkAlts (indVal : InductiveVal) (auxFunName : Name) :
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.BEq.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.BEq.mkMutualBlock (ctx : Context) :
TermElabM Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.BEq.mkBEqInstance (declName : Name) :
Command.CommandElabM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.BEq.mkBEqInstanceHandler (declNames : Array Name) :
Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.