leanprover/doc-gen4

@[reducible] attributes are not shown

alreadydone opened this issue · 1 comments

alreadydone commented

For example, the @[inline] attribute on Function.dcomp is shown but @[reducible] is not. On the other hand abbrevs are properly distinguished from defs.

hargoniX commented

Fixed locally:
image
coming to mathlib4_docs next build cycle.

  • 🎉1