Manipulating expressions with loose bvars

Stream: metaprogramming / tactics

[Markus de Medeiros]

I'm trying to generate Exprs of the shape fun x : T1 => fun y : T2 => ... f (g (x y)). I know all of my argument types T1 ... and the result type beforehand, and I have been able to get away with constructing the inner expression "by hand" so far (mkApp* does not seem to work when expressions have loose bvars). This is becoming quite painful when the types are dependent or have higher universes... what is the "right way" to construct such an expression?

[Henrik Böving]

By "right way" do you mean the one without loose bvars?

[Markus de Medeiros]

If such a thing exists, then sure! The problem is that the bvars are considered loose when constructing the inner expression even though I intend to close over them.

[Robin Arnez]

Something like

import Lean

def T2 : Type := Nat × Nat
def T1 : Type := T2 → Nat
def g : Nat → Int := fun x => x
def f : Int → Bool := fun x => x == 5

axiom «...» : Bool → Nat

open Lean Meta

def buildExpression : MetaM Expr := do
  withLocalDeclD `x (mkConst ``T1) fun x =>
  withLocalDeclD `y (mkConst ``T2) fun y =>
    let body := .app (mkConst ``«...») (.app (mkConst ``f) (.app (mkConst ``g) (.app x y)))
    mkLambdaFVars #[x, y] body

#eval do Lean.logInfo (← buildExpression)

The important things being docs#Lean.Meta.withLocalDeclD and docs#Lean.Meta.mkLambdaFVars

[Kyle Miller]

Expressions with loose bvars don't have very much support in the metaprogramming API; you're mostly on your own if you start working with them.

The intended way is to use free variables. For example, use withLocalDecl to enter a local context with a new free variable, then mkLambdaFVars to abstract an expression and close it as a lambda.

[Markus de Medeiros]

Perfect, this seems like exactly what I want! Thank you!

[Markus de Medeiros]

Ah... this is even one of the things covered in MPIL, I should have known this :sweat_smile: