match fvarid after ext

Stream: lean4

[Kenny Lau]

import Lean.Elab.Tactic.ElabTerm

open Lean Meta

elab "identify_fvar " id:ident : tactic => do
  let iID ← Lean.Elab.Tactic.getFVarId id
  logInfo m!"a: {iID.name}"
  have i := Expr.fvar iID
  logInfo m!"b: {i}"
  let typ ← inferType i
  logInfo m!"c: {typ}"

example (i : Nat) : 3 = 0 := by
  identify_fvar i -- a: _uniq.1131 // b: i // c: Nat

example (f g : Nat → Bool) : f = g := by
  ext i
  identify_fvar i -- a: _uniq.1209 // b: _fvar.1209 // unknown free variable `_fvar.1209`

[Kenny Lau]

I want to convert an identifier to an FVar, and it works for the first example, but it fails for the second example where the variable is introduced by ext. What's going on here?

[Aaron Liu]

Did you docs#Lean.Elab.Tactic.withMainContext

[Kenny Lau]

that works; what context was it using? i did some debugging and found that i was just entirely missing from the context

[Kenny Lau]

oh, it must have been just using the context that was just after by maybe

[Aaron Liu]

It uses the context at the beginning of the tactic seq I think (but don't rely on that)

[Kenny Lau]

thanks; i now have a custom tactic for destructing Fin n that is 10 times faster than fin_cases (i'm not kidding)

[Aaron Liu]

that's probably faster not after?

[Kenny Lau]

yes, corrected

[Aaron Liu]

Well fin_cases is kind of weird with what it does

[Aaron Liu]

I looked at the code since there was a bug and I saw the code and the bug is impossible very awkward to fix without a complete rewrite

[Aaron Liu]

It's not that complicated so a complete rewrite isn't too bad but