Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: unknown identifier error with user_notation


Etienne Laurin (Jan 29 2022 at 08:00):

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'

Last updated: Dec 20 2023 at 11:08 UTC