Where is `lambdaTelescopeReducing` located?

Stream: metaprogramming / tactics

[Gravifer]

I'm reading MPIL

There are many useful variants of `forallTelescope`:

- `forallTelescopeReducing`: like `forallTelescope` but matching is performed up
  to computation. This means that if you have an expression `X` which is
  different from but defeq to `∀ x, P x`, `forallTelescopeReducing X` will
  deconstruct `X` into `x` and `P x`. The non-reducing `forallTelescope` would
  not recognise `X` as a quantified expression. The matching is performed by
  essentially calling `whnf` repeatedly, using the ambient transparency.
- `forallBoundedTelescope`: like `forallTelescopeReducing` (even though there is
  no "reducing" in the name) but stops after a specified number of `∀` binders.
- `forallMetaTelescope`, `forallMetaTelescopeReducing`,
  `forallMetaBoundedTelescope`: like the corresponding non-`meta` functions, but
  the bound variables are replaced by new `mvar`s instead of `fvar`s. Unlike the
  non-`meta` functions, the `meta` functions do not delete the new metavariables
  after performing some computation, so the metavariables remain in the
  environment indefinitely.
- `lambdaTelescope`, `lambdaTelescopeReducing`, `lambdaBoundedTelescope`,
  `lambdaMetaTelescope`: like the corresponding `forall` functions, but for
  `λ` binders instead of `∀`.

Of which I cannot find lambdaTelescopeReducing in the Lean.Meta namespace or directly in source. Any pointers?

[Kenny Lau]

Lean.Meta.lambdaMetaTelescope maybe

[Jovan Gerbscheid]

Maybe nobody ever needed to use lambdaTelescopeReducing, so it doesn't exist?

[Chris Henson]

Jovan Gerbscheid said:

Maybe nobody ever needed to use lambdaTelescopeReducing, so it doesn't exist?

I tentatively reached the same conclusion. That paragraph was committed a few years ago, but even going back that far in the git history I couldn't find it. I think the author maybe just assumed every forall function had a lambda equivalent.

[Jannis Limperg]

Probably (says I as the author). ^^ For extra confusion, it seems like the lambda telescoping functions are all reducing. Please open an issue on the book repo.

[Jannis Limperg]

This is maybe as good a place as any to mention that the meta book could do with a lot of editing/rewriting/expanding, in case anyone is up for it. It's a perennial "one of these days" task for me.