3.1. Generated proof interfaces🔗

The previous chapter introduced the two interfaces used by the automation. A typed view hides the string-keyed capture map and exposes the fields used by values and constraints. Its generated normal forms connect that record to acceptance, denotation, parser success, and rejection.

A structural derivation retains the grammar choices that a view deliberately forgets. Valid derivations can be rendered and connected back to decoding, which makes them useful inputs to printer and roundtrip proofs. Automation works through these generated interfaces rather than unfolding the generic decoder.