structure Lean.Meta.GeneralizeTelescope.Entry : Type

• expr : Lean.Expr
• type : Lean.Expr
• modified : Bool

partial def Lean.Meta.GeneralizeTelescope.updateTypes (e : Lean.Expr) (eNew : Lean.Expr) (entries : Array Lean.Meta.GeneralizeTelescope.Entry) (i : Nat) : Lean.MetaM (Array Lean.Meta.GeneralizeTelescope.Entry)

partial def Lean.Meta.GeneralizeTelescope.generalizeTelescopeAux {α : Type} (k : Array Lean.Expr → Lean.MetaM α) (entries : Array Lean.Meta.GeneralizeTelescope.Entry) (i : Nat) (fvars : Array Lean.Expr) : Lean.MetaM α

def Lean.Meta.generalizeTelescope {α : Type} (es : Array Lean.Expr) (k : Array Lean.Expr → Lean.MetaM α) : Lean.MetaM α

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.