def Lean.Elab.Deriving.DecEq.mkDecEqHeader (indVal : InductiveVal) : TermElabM Header

Equations

• Lean.Elab.Deriving.DecEq.mkDecEqHeader indVal = Lean.Elab.Deriving.mkHeader `DecidableEq 2 indVal

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.

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.

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.

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.

def Lean.Elab.Deriving.DecEq.mkAuxFunctions (ctx : Context) : TermElabM (TSyntax `command)

Equations

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

def Lean.Elab.Deriving.DecEq.mkDecEqCmds (indVal : InductiveVal) : TermElabM (Array Syntax)

Equations

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

def Lean.Elab.Deriving.DecEq.mkDecEq (declName : Name) : Command.CommandElabM Bool

Equations

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

def Lean.Elab.Deriving.DecEq.mkEnumOfNat (declName : Name) : MetaM Unit

Equations

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

partial def Lean.Elab.Deriving.DecEq.mkEnumOfNat.mkDecTree (enumType : Expr) (ctors : Array Name) (n cond : Expr) (low high : Nat) : Expr

def Lean.Elab.Deriving.DecEq.mkEnumOfNatThm (declName : Name) : MetaM Unit

Equations

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

def Lean.Elab.Deriving.DecEq.mkDecEqEnum (declName : Name) : Command.CommandElabM Unit

Equations

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

def Lean.Elab.Deriving.DecEq.mkDecEqInstance (declName : Name) : Command.CommandElabM Bool

Equations

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

def Lean.Elab.Deriving.DecEq.mkDecEqInstanceHandler (declNames : Array Name) : Command.CommandElabM Bool

Equations

• Lean.Elab.Deriving.DecEq.mkDecEqInstanceHandler declNames = Array.foldlM (fun (b : Bool) (n : Lean.Name) => pure b <&&> Lean.Elab.Deriving.DecEq.mkDecEqInstance n) true declNames