Definition and notation for positive natural numbers #
Equations
- Eq (instPNatDecidableEq a b) (a.instDecidableEq b)
Instances For
ℕ+
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 "ℕ+"))
Instances For
Equations
- Eq instReprPNat { reprPrec := fun (n : PNat) (n' : Nat) => Repr.reprPrec n.val n' }