Lectures onType Theory
ch:very-dependent-functions: finite predecessor checking
appendix sectiontutorials

ch:very-dependent-functions: finite predecessor checking

Exercise 95.6.

Problem and invariant. Validate a finite declaration in numeric label order. Every dependency must be strictly smaller than its field label.

Two representations. A graph plus topological sort supports arbitrary orders; numeric labels make the predecessor witness explicit and let structural list recursion decide the frozen corpus directly.

First complete version. Define fields as label/dependency pairs. Write allBefore, lift it over declarations, then add Point, numeric, self-edge, cycle, and predecessor-visibility fixtures.

Observable result. The run ends All 5 Chapter 95 corpus cases passed.

A failing version. Replace < with . Self-dependency and visibility oracles fail; the test exits 1.

Acceptance and boundary. Apply the four commands of subappendix E.7 and require audit []. Numeric order checking does not construct or validate a very-dependent PER family.

Search the book

Type to search the local edition.