mathlib
e6e25d06
- cleanup(order|string) (#1629)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
6 years ago
cleanup(order|string) (#1629) move data.string to data.string.basic remove classical.decidable_linear_order. was duplicate of classical.DLO
References
#1629 - cleanup(order|string)
Author
fpvandoorn
Committer
mergify[bot]
Parents
b9e3dbba
Loading