unknown identifier error with user_notation

Stream: metaprogramming / tactics

[Etienne Laurin]

Hello! What is the proper way to capture free variables by name in a pexpr? Why does ok work but not bad?

meta def tactic.interactive.xₙ
  (_ : interactive.parse $ lean.parser.tk "=")
  (e₁ : interactive.parse interactive.types.texpr)
  : tactic unit :=
  tactic.to_expr ```(λ (n : ℕ), %%e₁) >>= tactic.exact

reserve prefix `xₙ`:100

@[user_notation]
meta def mk_seq_macro
  (_ : interactive.parse $ lean.parser.tk "xₙ")
  (_ : interactive.parse $ lean.parser.tk "=")
  (e₂ : interactive.parse interactive.types.texpr)
  : lean.parser pexpr :=
  pure ```(λ (n : ℕ), %%e₂)

def ok := by xₙ = n

def bad := xₙ = n  -- unknown identifier 'n'