Turn a term into a location

Stream: lean4

[Heather Macbeth]

I'm writing a macro and at some point I have a hypothesis (more precisely, a term which I mkIdent into a hypothesis) which I also want to consider as a location. How can I do this?

Example: I want a macro which combines the actions of the two lines foo and bar below.

import Mathlib.Tactic.Basic
import Mathlib.Tactic.Replace

theorem pow_eq_zero {a n : Nat} (h : a ^ n = 0) : a = 0 := sorry

open Lean Parser Tactic

macro "foo " h:location : tactic => `(tactic | change _ = 0 $h:location)

macro "bar " h:term : tactic =>
  let t := h.raw.getId;
  `(tactic | replace $(mkIdent t):ident := pow_eq_zero $(mkIdent t))

example (h : x ^ 3 = 1 - 1) : False := by
  foo at h
  bar h
  sorry

[Mac Malone]

This should work:

macro "foobar " h:term : tactic => do
  let hLoc ← `(location| at $h:term)
  `(tactic| {foo $hLoc; bar $h})

[Mac Malone]

Or more straightforwardly:

macro "foobar " h:term : tactic => do
  `(tactic| {foo at $h:term; bar $h})

[Heather Macbeth]

Thanks!

[Mac Malone]

@Heather Macbeth I actually messed up slightly. I should have used :term rather than the anon ctor. I have updated the examples.