Sig now does not depend on a telescope but is handled uniformly as the other binders. The Expr objects do not inherit fields from the info dictionary anymore, so one has to type e.info.my_field instead of e.my_field. This makes understanding errors much easier, as the e.my_field returned None when the field was not present in the dictionary.

Elab creates the basic framework for implicit types. Types can be marked as implicit, and when a term is applied to others, the elaboration function fills blanks with fresh meta-variables. Note that this will require duplicating type names: nat and nat_implicit, with identical names (but different tags).

The unification constraints are not solved for now.