Controlling forallTelescope

Stream: metaprogramming / tactics

[Adam Topaz]

Do we have a version of docs#Lean.Meta.forallTelescope which only "telescopes" the first n of the parameters?

[Adam Topaz]

Oh, I guess it's just forallTelescopeReducingAuxAux (reducing := false) (maxFVars? := some n) type k

[Thomas Murrills]

docs#Lean.Meta.forallMetaBoundedTelescope should do it :)

[Kyle Miller]

I think you mean docs#Lean.Meta.forallBoundedTelescope ?

[Kyle Miller]

(Something with AuxAux seems like something you shouldn't be using!)

[Thomas Murrills]

Ah, yes, mentally duplicated the Meta…

[Adam Topaz]

Kyle Miller said:

(Something with AuxAux seems like something you shouldn't be using!)

Yeah, I know, I just took a peek at the code for forallTelescope.

[Kyle Miller]

Note that forallBoundedTelescope reduces too, just like forallTelescopeReducing

[Adam Topaz]

hmm... I see, so we don't have a non-AuxAux version that does not reduce?

[Kyle Miller]

If you don't want it to reduce, it's up to you to give it an appropriate bound.

[Adam Topaz]

aha ok.

[Adam Topaz]

In practice my bound is 1, and I'm matching the expr on a forallE, so I think I should be ok.

[Eric Wieser]

I think if you're matching a single forallE, maybe Meta.withLocalDecl with instantiate1 suffices?

[Eric Wieser]

forallTelescope seems to be doing an awful lot of work for the case that is "I have one variable, please just introduce it without checking reducibility or anything"

[Kyle Miller]

It does turn out that there's something special about the telescope functions that withLocalDecl doesn't do, which I haven't appreciated until recently, and that's maintain the local instance cache.

[Kyle Miller]

I added a quick entry to https://github.com/leanprover-community/mathlib4/wiki/Metaprogramming-gotchas

I haven't observed this issue in practice yet, but it's good to know about I think. I feel like I need to review a bunch of my metaprograms...