-
Notifications
You must be signed in to change notification settings - Fork 189
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
Split HIT files into Core and lemmas #1855
Comments
Do you mean creating subdirectories for each type of colimit, like Colimits/GraphQuotient/*, Colimits/Coeq/*, Colimits/Colimit/*, Colimits/Pushout/*, etc? That might be ok, but it might also be overkill, since currently the only thing we separate are the flattening lemmas. |
@jdchristensen Yes that is what I meant. I'm fine with splitting the flattening lemmas into separate files too. One thing to keep in mind is that the flattening lemams are now much lighter so it might not be as big of an issue as before with the colimits library. I think we will have to see once those PRs are merged. |
We should split the various HIT files like GraphQuotient, Coeq, Pushout into separate files like we do for Join which will make the compilation faster.
Originally posted by @Alizter in #1851 (comment)
The text was updated successfully, but these errors were encountered: