Definition and notation for positive natural numbers

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 }

instance instDecidableEqPNat : DecidableEq ℕ+

Equations

• instDecidableEqPNat a b = a.instDecidableEq b

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 "ℕ+")

def PNat.val : ℕ+ → ℕ

The underlying natural number

Equations

• PNat.val = Subtype.val

instance coePNatNat : Coe ℕ+ ℕ

Equations

• coePNatNat = { coe := PNat.val }

instance instReprPNat : Repr ℕ+

Equations

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