mathlib3
24a8bb93
- feat(order/well-founded): Remove redundant arguments (#13702)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
3 years ago
feat(order/well-founded): Remove redundant arguments (#13702) All of these are inferred as `{α : Type*}` (as opposed to `{α : Sort*}`), and there is already a `variables {α : Type*}` at the top of the file.
Author
vihdzp
Parents
438b39a7
Loading