google-deepmind / google-deepmind/formal-conjectures
expose `category` attribute in doc-gen4
Open
documentation
enhancement
- Dominant language
- Lean
- Stars
- 1.3k
- Forks
- 485
- Avg merge
- 1d 20h
- Merged PRs (30d)
- 328
Description
Right now the information from the `category` attribute, like for instance
```lean
@[category research solved, AMS 11]
```
is not shown in the doc-gen4 output. It would be useful to access it in some way when reading doc-gen4 output without going to the source.
Contributor guide
Assessment
This issue has not been assessed yet.