Post

panproto
@panproto.dev

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.

0 reposts0 likes

panproto
@panproto.dev

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.

panproto
@panproto.dev

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.

panproto
@panproto.dev

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.

panproto
@panproto.dev

Didactic can attach an indexed family to Model fields. For example, a record with kind="number" can require a numeric body, and kind="text" can require text. Construction, JSON decoding, and immutable updates enforce the same cross-field dependency.