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 }

Instances For

• Int.canLiftPNat
• Nat.canLiftPNat
• PNat.instInhabited
• PNat.instWellFoundedRelation
• coePNatNat
• instOfNatPNatOfNeZeroNat
• instOnePNat
• instPNatLinearOrder
• instReprPNat

instance instPNatDecidableEq : DecidableEq ℕ+

Equations

• instPNatDecidableEq 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

Instances For

• Nat.canLiftPNat
• NeZero.pnat

instance coePNatNat : Coe ℕ+ ℕ

Equations

• coePNatNat = { coe := PNat.val }

instance instReprPNat : Repr ℕ+

Equations

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