Unknown constant 'Lean.Elab.Term.elabNumLit' on Go to Definition

Open mhuisi opened this issue 1 year ago • 2 comments

Use the following MWE and trigger Go to Definition at <cursor>:

#eval <cursor>1

This yields an error:

[Error - 11:37:43 AM] Request textDocument/definition failed.
  Message: unknown constant 'Lean.Elab.Term.elabNumLit'
  Code: -32603

I would not expect an error here.

Current nightly.

Add :+1: to issues you consider important. If others are impacted by this issue, please ask them to add :+1: to it.

Mar 27 '24 10:03 mhuisi

On leanprover/lean4:nightly-2024-04-21, I'm just getting a pop-up "No definition found for '1'". Can anyone else reproduce?

Apr 22 '24 06:04 kim-em

On leanprover/lean4:nightly-2024-04-21, I'm just getting a pop-up "No definition found for '1'". Can anyone else reproduce?

You get the popup, but you also get a server error under Output > Lean: Editor.

Apr 22 '24 09:04 mhuisi