forallBoundedTelescope

Stream: lean4

[Alice Laroche]

Is there a lambda equivalent for forallBoundedTelescope ?

[Daniel Fabian]

there's lambdaTelescope

[Alice Laroche]

Well, yes, but it's not bounded

[Leonardo de Moura]

Note that, forallBoundedTelescope may try to reduce the given type to make sure we have the requested number of binders. We rely on this feature in many different places. On the other hand, lambdaTelescope does not reduce the input expression. It just "consumes" the binders of the lambda expression. This is what we needed to implement Lean.
Note that it may be quite expensive to unfold arbitrary expressions, and we try to avoid it.

[Alice Laroche]

Hmm, so is there something like telescope, but for only one binder ?

[Leonardo de Moura]

We have withLocalDecl. Here are some code that may be useful

import Lean

namespace Lean.Meta

def lambdaBoundedTelescope (e : Expr) (n : Nat) (f : Array Expr → Expr → MetaM α) : MetaM α :=
  lambdaTelescope e fun xs e => do f xs[:n] (← mkLambdaFVars xs[n:] e)

def tst1 : MetaM Unit := do
  let ConstantInfo.defnInfo info ← getConstInfo ``List.map | unreachable!
  lambdaBoundedTelescope info.value 1 fun xs e => do
    IO.println (← ppExpr e)

#eval tst1

def lambdaTelescope1 (e : Expr) (f : Expr → Expr → MetaM α) : MetaM α := do
  let Expr.lam n t b d := e | throwError "lambda expected{indentExpr e}"
  withLocalDecl n d.binderInfo t fun x => f x (b.instantiate1 x)

def tst2 : MetaM Unit := do
  let ConstantInfo.defnInfo info ← getConstInfo ``List.map | unreachable!
  lambdaTelescope1 info.value fun x e => do
    IO.println (← ppExpr e)

#eval tst2

[Daniel Fabian]

there's also a withLocalDecls as a list version. Bit complicated type, because of dependent binders.