# 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

- ℕ+ = { n : ℕ // 0 < n }

Instances For

source
instance instDecidableEqPNat :
DecidableEq ℕ+
Equations

- instDecidableEqPNat a b = a.instDecidableEq b

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

- «termℕ+» = Lean.ParserDescr.node `«termℕ+» 1024 (Lean.ParserDescr.symbol "ℕ+")

Instances For

source
def PNat.val :
ℕ+ → ℕ

The underlying natural number

Equations

- PNat.val = Subtype.val

Instances For

source
instance coePNatNat :
Coe ℕ+ ℕ
Equations

- coePNatNat = { coe := PNat.val }

source
instance instReprPNat :
Repr ℕ+
Equations

- instReprPNat = { reprPrec := fun (n : ℕ+) (n' : ℕ) => reprPrec n.val n' }