Collecting binders

Stream: metaprogramming / tactics

[Leni Aniva]

I'm writing a tactic that extracts instances of v in the target and replaces them with a fvar, e.g.

|- 1 + v

becomes

x : ...
|- 1 + x

However, if there are binders involved, e.g.

|- (fun (a : A) => (forall (b : B), v b)) c

I would need to generate an x of type

x : forall (a : A) (b : B), V := fun (a : A) (b : B) => v

where v : V. Is there a telescope-like function that would allow me to do this? I can traverse to the position of v via Meta.transform or Meta.replaceSubexpr.

[Edward van de Meent]

do you know about Lean.Meta.lambdaTelescope?

[Edward van de Meent]

and similarly, Lean.Meta.forallTelescope

[Leni Aniva]

Edward van de Meent said:

do you konw about Lean.Meta.lambdaTelescope?

Yes, but in this case I may have both lambdas and foralls, and I wonder if there's a solution to this case. If its just lambda's or just forall's then its easy

[Leni Aniva]

e.g.

(fun (a : A) => mystery (forall (b : B), b v)) z

[Leni Aniva]

My current solution is I use one of the transform functions, and I compare what additional fvars went into the operand's lctx, and I abstract all of those fvars into lambda binders.

[Aaron Liu]

Leni Aniva said:

I would need to generate an x of type

x : fun (a : A) => forall (b : B), V

where v : V. Is there a telescope-like function that would allow me to do this? I can traverse to the position of v via Meta.transform or Meta.replaceSubexpr.

Is this a valid type for x?

[Leni Aniva]

Aaron Liu said:

Leni Aniva said:

I would need to generate an x of type

x : fun (a : A) => forall (b : B), V

where v : V. Is there a telescope-like function that would allow me to do this? I can traverse to the position of v via Meta.transform or Meta.replaceSubexpr.

Is this a valid type for x?

sorry I made a mistake. The type of x should be forall (a : A) (b : B), V, and its value should be fun (a : A) (b : B) => v