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.

[Patrick Massot]

Is there a version of forallBoundedTelescope that would give convenient access to the user names and types of the new local variables?

[Patrick Massot]

I want to replace boilerplate like

    Lean.Meta.forallBoundedTelescope type (some number)
          fun fvars _ ↦ do
        for fvar in fvars do
          let fvar := fvar.fvarId!
          let some decl := (← getLCtx).find? fvar | panic! "Something went wrong"
          …

[Marcus Rossel]

The various functions on docs#Lean.FVarId should improve the situation a tiny bit:
docs#Lean.FVarId.getType, docs#Lean.FVarId.getUserName

[Joachim Breitner]

Also inferType can be used. It feels more expensive to write that, but if the argument is known to be a fvar, it's just a lookup in the environment

[Patrick Massot]

Indeed those make the code a bit less ugly, but it still feels like we could have a more convenient way (but the meta-programming API is already so huge…).