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

[JadAbouHawili]

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