1726d37d4e
Add fields for decidable_eq and decidable_le. We need this because a concrete instance may have its own implementation that is not definitionally equal to the old ones defined at library/algebra/order.lean. Without this change, types such as nat and int would have multiple definitions for decidable_eq and decidable_le which are not definitionally equal. |
||
|---|---|---|
| .. | ||
| data | ||
| init | ||
| system | ||
| tools | ||
| .project | ||
| library.md | ||
| standard.lean | ||