lean4-htt/tests
Leonardo de Moura cfc46ac17f
feat: internalization for grind order (#10562)
This PR simplifies the `grind order` module, and internalizes the order
constraints. It removes the `Offset` type class because it introduced
too much complexity. We now cover the same use cases with a simpler
approach:
- Any type that implements at least `Std.IsPreorder`
- Arbitrary ordered rings.
- `Nat` by the `Nat.ToInt` adapter.
2025-09-26 03:49:06 +00:00
..
bench chore: update bench/riskv-ast.lean (#10505) 2025-09-24 11:46:26 +00:00
compiler chore: remove >6 month old deprecations (#10446) 2025-09-22 12:47:11 +00:00
elabissues
ir
lean feat: internalization for grind order (#10562) 2025-09-26 03:49:06 +00:00
pkg feat: list definitions in defeq problems that could not be unfolded for lack of @[expose] (#10158) 2025-09-23 16:13:39 +00:00
playground
plugin
simpperf
.gitignore
common.sh
lakefile.toml
lean-toolchain