Metaprograming: keeping track of "true" names bound vars

Stream: lean4

[Cody Roux]

Hi all! If I run this:

run_elab
  let t ← `(fun (x y : Int) => x + y)
  let e ← Lean.Elab.Term.elabTerm t none
  let v ← lambdaTelescope e
    (fun v _ => return v)
  Lean.logInfo s!"{v}"

I get somewhat inscrutable names. For various reasons; I'd like to get my hands on the original x and y. Is there any way to do this?

Other question: if I then later lambda over these generated names, do I get a term that looks nice?

[Aaron Liu]

this is the wrong way to do whatever you are trying to do

[Aaron Liu]

can you give some more information please about whatever you are trying to do

[Aaron Liu]

like for example those various reasons

[Floris van Doorn]

This might be closer to what you want:

import Lean

open Lean Meta Elab
run_elab do
  let t ← `(fun (x y : Int) => x + y)
  let e ← Lean.Elab.Term.elabTerm t none
  let v ← lambdaTelescope e fun v _ => do
    logInfo m!"{v}"

[Floris van Doorn]

(also #mwe)

[Cody Roux]

aha

[Floris van Doorn]

Note that the monads MetaM and TermElabM have a notion of local context (i.e. the hypotheses you see in the tactic state). This is part of the monad context. A function like lambdaTelescope modifies the context (it's different inside the program in its argument).
The variables v and _ that lambdaTelescope might not be well-typed inside the ambient context, and so operations on them will not work properly.

[Cody Roux]

to answer @Aaron Liu ; we have a bunch of code that's doing the "wrong" thing all over the place; I'm trying to incrementally move it to being the "right" thing.

[Cody Roux]

though going in to the details would be time consuming and would probably need me to understand more of the code than I currently do

[Aaron Liu]

incrementally?

[Floris van Doorn]

Actually the last line can be just logInfo m!"{v}" (editing that now)

[Floris van Doorn]

Note: m!"..." is the recommended way to print anything that involves expressions. It gives nice hovers in the InfoView.

[Cody Roux]

I see, thanks!

[Cody Roux]

Yes; for now I'm just trying to make the front end a little less crazy; at the moment it creates fresh variables wholesale, which it later lambdas over.

[Aaron Liu]

You may be looking for

• docs#Lean.mkFreshFVarId
• docs#Lean.Meta.withLocalDecl
• docs#Lean.Meta.lambdaTelescope

[Cody Roux]

Thanks!