Documentation

Lean.Elab.Deriving.DecEq

Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
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 Lean.Name) (n : Lean.Expr) (cond : Lean.Expr) (low : Nat) (high : Nat) :
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.