Documentation

Lean.Elab.Deriving.Repr

source
def Lean.Elab.Deriving.Repr.mkReprHeader (indVal : InductiveVal) :
TermElabM Header
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Repr.mkBodyForStruct (header : Header) (indVal : InductiveVal) :
TermElabM Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Repr.mkBodyForInduct (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.Repr.mkBodyForInduct.mkAlts (header : Header) (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.Repr.mkBody (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.Repr.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.Repr.mkMutualBlock (ctx : Context) :
TermElabM Syntax
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.Repr.mkReprInstanceHandler (declNames : Array Name) :
Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.