Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Auto-generated lemmas appear before declaration #163

Open
alreadydone opened this issue Nov 14, 2023 · 1 comment
Open

Auto-generated lemmas appear before declaration #163

alreadydone opened this issue Nov 14, 2023 · 1 comment

Comments

@alreadydone
Copy link

alreadydone commented Nov 14, 2023

For example, FundamentalGroupoid.ext_iff appears before FundamentalGroupoid, completelyRegularSpace_iff appears before CompletelyRegularSpace, Pi.nonUnitalRingHom_apply appears before Pi.nonUnitalRingHom. These are due to the attributes @[ext], @[mk_iff], and @[simps] respectively. The additive version produced by @[to_additive] also comes before the multiplicative version (e.g. EckmannHilton.AddZeroClass.IsUnital) but those don't necessitates a fix.

(Inspired by #161 which is also about ordering)

@alreadydone alreadydone changed the title Auto-generated lemmas appear before declaration in docs Auto-generated lemmas appear before declaration Nov 14, 2023
@hargoniX
Copy link
Collaborator

doc-gen sorts declarations according to their declared line number:

res := res.insert moduleName {module with members := module.members.qsort ModuleMember.order}
if the declared line number of the generated things was below the original things it would sort correctly.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants