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

Equations

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

def Lean.Elab.Deriving.DecEq.mkMatch (ctx : Lean.Elab.Deriving.Context) (header : Lean.Elab.Deriving.Header) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM Lean.Term

Equations

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

def Lean.Elab.Deriving.DecEq.mkMatch.mkSameCtorRhs : List (Lean.Ident × Lean.Ident × Option Lake.Name × Bool) → Lean.Elab.TermElabM Lean.Term

Equations

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

def Lean.Elab.Deriving.DecEq.mkMatch.mkAlts (ctx : Lean.Elab.Deriving.Context) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM (Array (Lean.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 : Lean.Elab.Deriving.Context) (auxFunName : Lake.Name) (indVal : Lean.InductiveVal) : Lean.Elab.TermElabM (Lean.TSyntax `command)

Equations

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

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

Equations

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

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.

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

Equations

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

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

Equations

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

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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