Documentation

Given expressions es := #[e_1, e_2, ..., e_n], execute k with the free variables (x_1 : A_1) (x_2 : A_2 [x_1]) ... (x_n : A_n [x_1, ... x_{n-1}]). Moreover,

• type of e_1 is definitionally equal to A_1,
• type of e_2 is definitionally equal to A_2[e_1].
• ...
• type of e_n is definitionally equal to A_n[e_1, ..., e_{n-1}].

This method tries to avoid the creation of new free variables. For example, if e_i is a free variable x_i and it is not a let-declaration variable, and its type does not depend on previous e_js, the method will just use x_i.

The telescope x_1 ... x_n can be used to create lambda and forall abstractions. Moreover, for any type correct lambda abstraction f constructed using mkForall #[x_1, ..., x_n] ..., The application f e_1 ... e_n is also type correct.

The kabstract method is used to "locate" and abstract forward dependencies. That is, an occurrence of e_i in the of e_j for j > i.

The method checks whether the abstract types A_i are type correct. Here is an example where generalizeTelescope fails to create the telescope x_1 ... x_n. Assume the local context contains (n : Nat := 10) (xs : Vec Nat n) (ys : Vec Nat 10) (h : xs = ys). Then, assume we invoke generalizeTelescope with es := #[10, xs, ys, h] A type error is detected when processing h's type. At this point, the method had successfully produced

  (x_1 : Nat) (xs : Vec Nat n) (x_2 : Vec Nat x_1)

and the type for the new variable abstracting h is xs = x_2 which is not type correct.