How to elaborate local notation?

Stream: new members

[Jakub Nowak]

How can I elaborate terms in the context of local variables?

import Lean

variable (n : Nat)

local notation "ι" => n

/-- error: Unknown constant `n✝` -/
#guard_msgs in
open Lean Elab.Term in
run_elab
  elabTerm (← `(ι)) none

[Jakub Nowak]

Although, maybe the issue is not with elabTerm, but the fact that the syntax in `(ι) is not parsed in the context of local variables?

[Jakub Nowak]

I still don't know how to make this code work though. .-.

[Kyle Miller]

Local variables are a command elaborator concept. You can use docs#Lean.Elab.Command.runTermElabM to elaborate the local variables and get into a context where they exist.