Post

We have new versions of panproto (0.74) and didactic (0.15). didactic adds a public general first-order generalized algebraic data type (GADT) and indexed-family language, and panproto checks the resulting theory.

You can now declare arbitrary indexed families, such Vec(n), Expr(t), Matrix(rows, columns), or Term(context, type). Family parameters form dependent telescopes, so a later parameter may depend on an earlier one.

Constructors may refine result indices. For instance: nil : Vec(0) and cons : A × Vec(n) → Vec(succ n). Panproto uses those refinements during type checking. A constructor or branch at the wrong index is rejected.

User-defined eliminators may have dependent motives. eval : Expr(t) → El(t) is checked branch by branch after refining t. Returning an integer carrier from a Boolean expression branch is a type error.

Implicit indices now work in eliminator equations. head : Vec(succ n) → A can omit n at the call site. panproto can infer it from the vector. The nil case is impossible. Including it is rejected as unreachable.