Kim Morrison 20acc72a29 feat: ensure Fin.foldl/r are semireducible (#6207) ... This PR ensures the `Fin.foldl` and `Fin.foldr` are semireducible. Without this the defeq `example (f : Fin 3 → ℕ) : List.ofFn f = [f 0, f 1, f 2] := rfl` was failing. Thanks @eric-wieser and @digama0 for diagnosing on [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/.60List.2EfinRange.60.20in.20Mathlib/near/484191814).		2024-11-25 03:21:36 +00:00
..
bench	feat: Array.swap takes Nat arguments, with tactic provided proofs (#6194)	2024-11-24 07:59:57 +00:00
compiler	feat: Nat.(fold|foldRev|any|all)M? take a function which sees the upper bound (#6139)	2024-11-22 03:05:51 +00:00
elabissues
ir
lean	feat: ensure Fin.foldl/r are semireducible (#6207)	2024-11-25 03:21:36 +00:00
pkg	fix: make sure monad lift coercion elaborator has no side effects (#6024)	2024-11-13 16:22:31 +00:00
playground	feat: rename Array.shrink to take, and relate to List.take (#5796)	2024-10-21 23:35:32 +00:00
plugin	chore: when a linter crashes, prefix its name (#4967)	2024-08-12 02:36:42 +00:00
simpperf
.gitignore
common.sh
lean-toolchain