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

• Eq PNat (Subtype fun (n : Nat) => LT.lt 0 n)

def instPNatDecidableEq : DecidableEq PNat

Equations

• Eq (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

• Eq «termℕ+» (Lean.ParserDescr.node `«termℕ+» 1024 (Lean.ParserDescr.symbol "ℕ+"))

def PNat.val : PNat → Nat

The underlying natural number

Equations

• Eq PNat.val Subtype.val

def coePNatNat : Coe PNat Nat

Equations

• Eq coePNatNat { coe := PNat.val }

def instReprPNat : Repr PNat

Equations

• Eq instReprPNat { reprPrec := fun (n : PNat) (n' : Nat) => Repr.reprPrec n.val n' }