RFC: Attributes in `#print`

[digama0]

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[Kha]

This RFC looks incomplete: it should discuss whether the intention is to print the attributes at the time of declaration or at the time of use, and the pros and cons of this decision.

[digama0]

The implementation in #6115 prints attributes at time of use.

[kim-em]

@digama0, would you be able to write something explaining why you prefer that choice? (Which, indeed, seems the more useful one to me.)