mathlib
6b63c034
- fix(order/rel_classes): remove looping instance (#8931)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
fix(order/rel_classes): remove looping instance (#8931) This instance causes loop with `is_total_preorder.to_is_total`, and was unused in the library. Caught by the new linter (#8932).
Author
fpvandoorn
Parents
53f074ca
Loading