reflection inside rw

Stream: general

[Kenny Lau]

let's say I have this:

theorem test : 1 = 0 :=
by rw [by (tactic.get_goals >>= tactic.trace)]

it seems like tactic.get_goals >>= tactic.trace cannot see the state outside (i.e. 1 = 0)

[Kenny Lau]

is there a way to access the outer scope from within rw?

[Keeley Hoek]

No