RFC: Attributes in `#print`

Proposal

In Lean 3, #print would show the attributes on a definition, such as @[reducible] or @[simp]. We should get this back. I think the only blocker here is a technical one.

@[reducible, simp] def foo := 1

#print foo
-- @[reducible] def Lean.Compiler.foo : Nat :=
-- 1

Currently a few attributes like @[reducible] are supported, but not others like @[simp], as demonstrated above.

Because the interest of #print is in seeing how lean views a declaration (and not merely copying the text of the input), I suggest this shows attributes relevant at the time of use, not the time of declaration. (In any case, in lean it is difficult to implement the latter.) The implementation in #6115 does not show scoped and local for attributes, and it does not show attributes at all if they were local and are now out of scope. These are both due to implementation issues, but the former seems easier to fix than the latter.

Community Feedback

This comes up periodically on Zulip, here is the latest thread.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Begin with the #print behavior described here and compare it with the implementation in #6115; no source file or test is identified in the issue. Done means #print shows applicable attributes such as reducible and simp, with the scoped and local behavior resolved as specified.