Zulip Chat Archive

Stream: general

Topic: attributes in docs


Reid Barton (Nov 25 2020 at 17:52):

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 (Nov 25 2020 at 17:57):

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

Gabriel Ebner (Nov 25 2020 at 17:57):

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

Rob Lewis (Nov 25 2020 at 17:58):

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 (Nov 25 2020 at 18:06):

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

Reid Barton (Nov 25 2020 at 18:06):

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

Gabriel Ebner (Nov 25 2020 at 18:22):

That's _refl_lemma.


Last updated: Dec 20 2023 at 11:08 UTC