elaborate a theorem without clashing

Stream: general

[Damiano Testa]

Often, writing linters, I want to take some theorem, modify it and elaborate it again. However, this causes problems, since the environment already contains the declaration name. I have a couple of workarounds for this (adding a namespace to the scope, replacing the declaration name by a fresh one, replacing the theorem by an example), but none of these is really satisfactory.

Is there a principled way to do this?

Here is some sample code:

import Lean.Elab.Command
import Batteries.Lean.Syntax

open Lean Elab Command in
elab "toIntro " cmd:command : command => do
  elabCommand cmd
  -- the next command is superfluous, I could have simply reelaborated `cmd`, but maybe it
  -- gives some context
  let newCmd ← cmd.replaceM fun s => if s.isOfKind ``Lean.Parser.Tactic.intros then
    return some (← `(tactic| intro)) else return none
  logInfo m!"Elaborating {newCmd}"
  elabCommand newCmd

/-
Elaborating theorem with_intros : ∀ x : Nat, x = x := by
  intro
  rfl
-/
toIntro
theorem with_intros : ∀ x : Nat, x = x := by  -- 'with_intros' has already been declared
  intros
  rfl

[Eric Wieser]

withoutModifyingState ?

[Eric Wieser]

That is, do the first elaboration in a context where everything (except your return value) is discarded

[Damiano Testa]

Unfortunately, with linters, the first elaboration is already done for you, so I'm stuck having to elaborate the second one.

[Damiano Testa]

Or, alternatively, is there a way to get the linter to run before the corresponding command is elaborated?