Tags: leanprover/lean4-nightly
Tags
feat: remove unnecessary decidability requirements (#9096) This PR removes some unnecessary `Decidable*` instance arguments by using lemmas in the `Classical` namespace instead of the `Decidable` namespace. This might lead to some additional dependency on classical axioms, but large parts of the standard library are relying on them either way.
feat: further release automation (#9092) This PR further updates release automation. The per-repository update scripts `script/release_steps.py` now actually performs the tests, rather than outputting a script for the release manager to run line by line. It's been tested on `v4.21.0` (i.e. the easy case of a stable release), and we'll debug its behaviour on `v4.22.0-rc1` tonight.
feat: support for `LawfulEqCmp` in `grind` (#9069)
This PR implements support for the type class `LawfulEqCmp`. Examples:
```lean
example (a b c : Vector (List Nat) n)
: b = c → a.compareLex (List.compareLex compare) b = o → o = .eq → a = c := by
grind
example [Ord α] [Std.LawfulEqCmp (compare : α → α → Ordering)] (a b c : Array (Vector (List α) n))
: b = c → o = .eq → a.compareLex (Vector.compareLex (List.compareLex compare)) b = o → a = c := by
grind
```
PreviousNext