Consume let

Stream: metaprogramming / tactics

[Adam Topaz]

What's the preferred way to "consume" a let in a Lean.Expr? For example, I would like the expr associated to let x := 2; x to become 2. Is there something I'm not seeing that prevents such a function from existing?

[Mario Carneiro]

depending on exactly how rigidly you want to do that and only that, you can match on the expr to see if it is .letE val type body and then return body.instantiate1 val

[Damiano Testa]

Also, docs#Mathlib.Tactic.unfoldFVars may get you close.

[Damiano Testa]

E.g., this works:

import Mathlib.Tactic.DefEqTransformations

open Lean Mathlib Elab Tactic
example : let x := 2; x = 2 := by
  intro x
  run_tac Lean.Elab.Tactic.withMainContext do  -- `2 = 2`
    let tgt ← getMainTarget
    let xv := ((← getLCtx).findFromUserName? `x).get!
    logInfo (← unfoldFVars #[xv.fvarId] tgt)
  dsimp

[Adam Topaz]

Thanks for the answers!

[Kyle Miller]

As a case study for what Mario said, the way whnf handles it is exactly that:

| .letE _ _ v b _ => if config.zeta then go <| b.instantiate1 v else return e