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.