interpolating localDecls into syntax quotations

Stream: metaprogramming / tactics

[Eric Wieser]

What's the right way of writing quick tactics like this?

import Lean
import Batteries.Lean.Expr

open Lean Meta Elab Tactic

example (a b c : Nat) (ha : a = 1) (hb : b = 1) (hc : c = 1) : True := by
  -- flip them all
  replace ha := ha.symm
  replace hb := hb.symm
  replace hc := hc.symm

  -- now do the same thing in a loop
  run_tac do
    for n in [`ha, `hb, `hc] do
      let d ← getLocalDeclFromUserName n
      let s := mkIdent d.userName
      let ds : Term ← d.toExpr.toSyntax
      evalTactic <| ← `(tactic| replace $s := $(ds).symm)
  sorry

The above fails with

synthetic hole has already been defined and assigned to value incompatible with the current context
  ha

[Damiano Testa]

withMainContext?

[Damiano Testa]

I.e.

import Lean
import Batteries.Lean.Expr

open Lean Meta Elab Tactic

example (a b c : Nat) (ha : a = 1) (hb : b = 1) (hc : c = 1) : True := by
  -- flip them all
  replace ha := ha.symm
  replace hb := hb.symm
  replace hc := hc.symm

  -- now do the same thing in a loop
  run_tac withMainContext do
    for n in [`ha, `hb, `hc] do
      let d ← getLocalDeclFromUserName n
      let s := mkIdent d.userName
      let ds : Term ← d.toExpr.toSyntax
      evalTactic <| ← `(tactic| replace $s := $(ds).symm)
  /-
  ha: a = 1
  hb: b = 1
  hc: c = 1
  -/
  sorry