Documentation

Mathlib.Data.PNat.Notation

Definition and notation for positive natural numbers #

source
🔸 coverage
def PNat :
Type

ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

Instances For
    source
    🔸 coverage
    @[implicit_reducible]
    instance instDecidableEqPNat :
    DecidableEq ℕ+
    source
    🔸 coverage
    def «termℕ+» :
    Lean.ParserDescr

    ℕ+ is the type of positive natural numbers. It is defined as a subtype, and the VM representation of ℕ+ is the same as ℕ because the proof is not stored.

    Instances For
      source
      🔸 coverage
      def PNat.val :
      ℕ+ → ℕ

      The underlying natural number

      Instances For
        source
        🔸 coverage
        @[implicit_reducible]
        instance coePNatNat :
        Coe ℕ+ ℕ
        source
        🔸 coverage
        @[implicit_reducible]
        instance instReprPNat :
        Repr ℕ+