2. Walkthrough: the Decimal format, end to end🔗

This chapter follows Cedar Decimal from its triptych input to the generated surface, typed view, parser, and integration theorems. Every Lean block is elaborated against the current generated files when this book builds.

1. 2.1. The format
2. 2.2. Artifact one: the readable spec
3. 2.3. Artifact two: the executable parser
4. 2.4. Artifact three: proof obligations
5. 2.5. Independent check against Cedar's test corpus