¹The decimal representation of natural numbers is just syntactic sugar for their Peano notation, whose constructors are 0 and the successor s, as explained in Section 8.3. Hence, a natural number is a tower of s symbols followed by a 0, which are efficiently supported using the iter attribute (see Section 4.4.2).