attributes in docs

Stream: general

[Reid Barton]

Some attributes don't show up in the generated documentation that probably should. At least [reducible] and [irreducible], and whatever abbreviation is exactly.

[Gabriel Ebner]

On the other hand @[nolint] is shown in the docs, but I don't think is very useful.

[Gabriel Ebner]

Feel free to file an issue at https://github.com/leanprover-community/doc-gen, or even better, a PR!

[Rob Lewis]

https://github.com/leanprover-community/doc-gen/blob/master/src/export_json.lean#L230 is the relevant line. The norm_cast attribute list is outdated, they should all be replaced by just norm_cast.

[Reid Barton]

If ext is in the list then maybe there's a case also for refl, symm, trans?

[Reid Barton]

What about whatever the attribute is that marks a rfl-lemma? That one would be extremely common, so maybe too noisy.

[Gabriel Ebner]

That's _refl_lemma.