Unknown introduced variables

Stream: lean4

[Abdalrhman M Mohamed]

I am working on an smt tactic for Lean 4 and I am getting an error when I call inferType on variables introduced by the intro tactic. Here is an isolated example:

import Lean

open Lean.Meta
open Lean.Elab
open Lean.Elab.Tactic

syntax (name := test) "test" : tactic

@[tactic test] def evalTest : Tactic := fun _ => do
  let g ← Tactic.getMainTarget
  let x := g.appFn!.appArg!.appArg!
  logInfo m!"goal := {g}, x := {x}"
  let xt ← inferType x
  logInfo m!"xt := {xt}"

theorem zero_sub : ∀ x : Nat, 0 - x = 0 := by
  intro x
  test
  induction x <;> simp_all [Nat.sub_succ]

For this example, I get the error: unknown free variable '_uniq.577'. Does anyone know how to resolve this error?

[Sebastian Ullrich]

Take a look at the function defined right below getMainTarget :) . withMainContext is normally used via liftMetaTactic, which splits the tactic implementation into a TacticM and a MetaM part. See the stdlib tactics for many examples.