Documentation

Lean.Elab.Deriving.DecEq

source
def Lean.Elab.Deriving.DecEq.mkDecEqHeader (indVal : InductiveVal) :
TermElabM Header
Equations
source
def Lean.Elab.Deriving.DecEq.mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) :
TermElabM Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs :
List (Ident × Ident × Option Name × Bool) → TermElabM Term
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.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.
source
def Lean.Elab.Deriving.DecEq.mkAuxFunction (ctx : Context) (auxFunName : Name) (indVal : InductiveVal) :
TermElabM (TSyntax `command)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkAuxFunctions (ctx : Context) :
TermElabM (TSyntax `command)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkDecEqCmds (indVal : InductiveVal) :
TermElabM (Array Syntax)
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkDecEq (declName : Name) :
Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkEnumOfNat (declName : Name) :
MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
partial def Lean.Elab.Deriving.DecEq.mkEnumOfNat.mkDecTree (enumType : Expr) (ctors : Array Name) (n cond : Expr) (low high : Nat) :
Expr
source
def Lean.Elab.Deriving.DecEq.mkEnumOfNatThm (declName : Name) :
MetaM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkDecEqEnum (declName : Name) :
Command.CommandElabM Unit
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkDecEqInstance (declName : Name) :
Command.CommandElabM Bool
Equations
  • One or more equations did not get rendered due to their size.
source
def Lean.Elab.Deriving.DecEq.mkDecEqInstanceHandler (declNames : Array Name) :
Command.CommandElabM Bool
Equations