Going under exactly one lambda

Stream: Is there code for X?

[Joachim Breitner]

In MetaM, for going under forall quantifiers, we have docs#Lean.Meta.forallTelescope that goes under as many foralls as possible, but also the more principled docs#Lean.Meta.forallMetaBoundedTelescope that goes under at most $n$ foralls.

But for opening up lambdas, I only see docs#Lean.Meta.lambdaTelescope, but no bounded variant, and I'd be mildly surprised that none ever had a need for that. How do you open up fixed number of lambda? (Or just exactly one, for that matter?)

[Kyle Miller]

If you know your expression is a lambda or a forall, here's a function that wraps up the pattern you normally see:

open Lean Meta in
def Lean.Expr.withLambda {α : Type _} (e : Expr) (k : Expr → Expr → MetaM α) : MetaM α :=
  withLocalDecl e.bindingName! e.bindingInfo! e.bindingDomain! fun fvar =>
    k fvar (e.bindingBody!.instantiate1 fvar)

[Kyle Miller]

(I think you meant to link to docs#Lean.Meta.forallBoundedTelescope instead of docs#Lean.Meta.forallMetaBoundedTelescope)

[Kyle Miller]

I think it would make sense to have a docs#Lean.Meta.lambdaBoundedTelescope

One design question is whether, like forallTelescope vs forallBoundedTelescope, the lambdaBoundedTelescope version would also do whnf if the expression isn't obviously a lambda. The forallBoundedTelescope is a controlled version of forallTelescopeReducing.

[Mario Carneiro]

Actually, that's not the only option, it could also manufacture lambdas that aren't there using eta expansion. This is what the compiler usually has to do when expecting an expression with a given arity

[Joachim Breitner]

Yes, that sounds even more useful, also because one can then expect that function to always return an array of exactly the expected length.

[Mario Carneiro]

well, not necessarily, e may not have the right type (although maybe in this case the function may be justified to throw an error)

[Joachim Breitner]

Yup, that's what I mean

[Joachim Breitner]

In a sense the dual of the function that I added here:
https://github.com/leanprover/lean4/pull/2902/files#diff-7714aba4907fdd09f34e5285d6ceebb090b89757fdc60bc1dcaf9c112bdf5228R93-R111

[Mario Carneiro]

I have an implementation here although it's also tied up with other stuff relating to its use in the compiler

[Joachim Breitner]

I have a few places where I could use that function. Once you are happy with it, will you PR it?