search

leanprover / lean4

Lean 4 programming language and theorem prover
https://lean-lang.org
Apache License 2.0
4.04k stars 348 forks source link

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

Open mhuisi opened 3 months ago

mhuisi commented 3 months ago

Description

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.

Versions

Current nightly.

Impact

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

semorrison commented 2 months ago

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

mhuisi commented 2 months ago

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.