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.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.

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