[Typo] 3.1.6.1. Another Representation , Type Signature of `succ`

Here's the quote:

 An alternative way to represent a positive number is as the successor of some Nat. Replace the definition of Pos with a structure whose constructor is named succ that contains a Nat:

structure Pos where
  succ ::
  pred : Nat

Define instances of Add, Mul, ToString, and OfNat that allow this version of Pos to be used conveniently.

I'm not sure what pred : Nat is for, isn't

structure PosAnswer where
succ : Nat \imp PosAnswer

enough to represent positive natural numbers? Nat starts from zero , the above PosAnswer would start from one.

I saw the constructor :: notation being used in Lean , like

structure And (a b : Prop) : Prop where
  /-- `And.intro : a → b → a ∧ b` is the constructor for the And operation. -/
  intro ::

but I'm not sure what in means in structure Pos

Start with the documentation section titled “3.1.6.1. Another Representation, Type Signature of succ” and compare the quoted Pos structure with the surrounding explanation. Done means the reported typo or notation issue is resolved and the purpose of pred : Nat is clear to readers.