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
[Merged by Bors] - feat: port fin_cases #437
Conversation
I'm not enthused about this implementation, it has a lot of potential failure modes, but since it's not passing all the tests or implementing all the options we'll need to extend it later anyway, and this is good enough for now. bors r+ |
Build failed: |
The implementation is pretty much isomorphic to the one in mathlib3, so I'll blame the author of that. (Err... sorry.) After I merge master it is all failing, with metavariables in the declarations, and I'm not immediately seeing why. |
Ugh, voodoo changing a Currently, if you call |
Okay, at least superficially fixed that, now we don't catch the error if |
bors merge |
Pull request successfully merged into master. Build succeeded: |
This is a port of
fin_cases
. It doesn't yet support thewith
orusing
clauses from mathlib3.I could remove the dependence on #433, but would have to (temporarily) remove all the tests to do so.
Fintype (Fin n)
#433