Documentation

Lean.Elab.Deriving.DecEq

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    Instances For
      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) :