747262e498
This PR makes `#print` show the full internal private name (including module prefix) in the declaration signature when `pp.privateNames` is set to true. Previously, `pp.privateNames` only affected names in the body but the signature always stripped the private prefix. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
48 lines
826 B
Text
48 lines
826 B
Text
module
|
|
|
|
-- Test that `pp.privateNames` affects the name in the output of `#print`, `#print sig`, and `#check`.
|
|
|
|
private def foo : Nat := 42
|
|
|
|
-- Without pp.privateNames, commands show the user name
|
|
/--
|
|
info: private def foo : Nat :=
|
|
42
|
|
-/
|
|
#guard_msgs in
|
|
#print foo
|
|
|
|
/--
|
|
info: private def foo : Nat
|
|
-/
|
|
#guard_msgs in
|
|
#print sig foo
|
|
|
|
/--
|
|
info: foo : Nat
|
|
-/
|
|
#guard_msgs in
|
|
#check @foo
|
|
|
|
-- With pp.privateNames, commands should show the full private name
|
|
set_option pp.privateNames true in
|
|
/--
|
|
info: private def _private.elab.printPrivate.0.foo : Nat :=
|
|
42
|
|
-/
|
|
#guard_msgs in
|
|
#print foo
|
|
|
|
set_option pp.privateNames true in
|
|
/--
|
|
info: private def _private.elab.printPrivate.0.foo : Nat
|
|
-/
|
|
#guard_msgs in
|
|
#print sig foo
|
|
|
|
set_option pp.privateNames true in
|
|
/--
|
|
info: _private.elab.printPrivate.0.foo : Nat
|
|
-/
|
|
#guard_msgs in
|
|
#check @foo
|