Specification

The specification is written in literate Agda and Typst (the same sources are type-checked by Agda and rendered to PDF by Typst) and lives in the spec/ directory of this repository. You can view the rendered version below or download it for fullscreen viewing here. See Agda formalisation for how the specification is machine-checked and kept in sync with the implementation.