Documentation

Lean.Elab.Deriving.DecEq

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