# Documentation

Lean.Meta.GeneralizeTelescope

Instances For
partial def Lean.Meta.GeneralizeTelescope.updateTypes (e : Lean.Expr) (eNew : Lean.Expr) (entries : ) (i : Nat) :
partial def Lean.Meta.GeneralizeTelescope.generalizeTelescopeAux {α : Type} (k : ) (entries : ) (i : Nat) (fvars : ) :
def Lean.Meta.generalizeTelescope {α : Type} (es : ) (k : ) :

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.

Equations
• One or more equations did not get rendered due to their size.