Documentation

Mathlib.Data.PNat.Notation

Definition and notation for positive natural numbers #

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

Equations
    Instances For
      source
      instance instPNatDecidableEq :
      DecidableEq ℕ+
      Equations
        source
        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.

        Equations
          Instances For
            source
            def PNat.val :
            ℕ+ → ℕ

            The underlying natural number

            Equations
              Instances For
                source
                instance coePNatNat :
                Coe ℕ+ ℕ
                Equations
                  source
                  instance instReprPNat :
                  Repr ℕ+
                  Equations