This PR fixes a bug in the `LinearOrderPackage.ofOrd` factory. If there is a `LawfulEqOrd` instance available, it should automatically use it instead of requiring the user to provide the `eq_of_compare` argument to the factory. The PR also solves a hygiene-related problem making the factories fail when `Std` is not open. |
||
|---|---|---|
| .. | ||
| bench | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||