Joachim Breitner ac64cfd70a fix: array_get_dec etc. tactics to solve more cases (#5037) ... Using `Nat.lt_trans` is too restrictive, and using `Nat.lt_of_lt_of_le` should make this tactic prove more goals. This fixes a regression probably introduced by #3991; at least in some cases before that `apply sizeOf_get` would have solved the goal here. And it’s true that this is now subsumed by `simp`, but because of the order that `macro_rules` are tried, the too restrictive variant with `Nat.lt_trans` would be tried before `simp`, without backtracking. Fixes #5027		2024-08-14 12:41:14 +00:00
..
bench	chore: speedcenter: reduce number of runs for "fast" benchmarks from 10 to 3 (#5009)	2024-08-13 09:06:06 +00:00
compiler	fix: split libleanshared on Windows to avoid symbol limit	2024-08-12 14:14:42 +02:00
elabissues
ir
lean	fix: array_get_dec etc. tactics to solve more cases (#5037)	2024-08-14 12:41:14 +00:00
pkg	feat: accept user-defined options on the cmdline (#4741)	2024-08-02 12:24:56 +00:00
playground
plugin	chore: when a linter crashes, prefix its name (#4967)	2024-08-12 02:36:42 +00:00
simpperf
.gitignore
common.sh
lean-toolchain