Commit 2026-03-26 01:43 0c43cd02

fix: improve recall impl / error reporting (#8740) This PR fixes recall to work inside namespaces and with open declarations, as reported on Zulip. Previously, recall used raw id.getId to extract the declaration name, which ignored the current namespace. Now it uses resolveGlobalConstNoOverload, the standard Lean name resolution function.

-- Previously failed with "Unknown constant 'myDef'"
namespace Foo
def myDef := 42
end Foo
namespace Foo
recall myDef : Nat  -- now works
end Foo
-- Also works with `open`
open Foo in
recall myDef : Nat

🤖 Prepared with Claude Code