lean4

lean4 copied to clipboard

Prerequisites

• [x] Put an X between the brackets on this line if you have done all of the following:
  • Checked that your issue isn't already filed.
  • Reduced the issue to a self-contained, reproducible test case.

Description

import Lean
open Lean Elab Command

open Parser

elab "hmmm" arg:(ppSpace ident)+ : command =>
  -- arg has type `Option (TSyntax Name.anonymous)`
  logInfo (toString arg)

hmmm xyz

This prints #[(group `xyz)] when the Parser namespace is open. If you comment out the open Parser, then it prints #[`xyz].

I would expect it to always print #[`xyz].

Versions

Nightly from June 30.

Hmm yes, this is https://github.com/leanprover/lean4/pull/1229#discussion_r900885634 :( . The best workaround I see is to make sure we always default to the alias.

The best workaround I see is to make sure we always default to the alias.

@gebner What do you think? Is that satisfactory until we improve Parser?

So resolve to the alias first, and only look it up as a declaration if that fails? That seems good to me.