max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Init/Data/Array
History
Leonardo de Moura 186a81627b
fix: Array.foldlMUnsafe bug (#11772) 
This PR a bug in the optimized and unsafe implementation of
`Array.foldlM`.

Issue was reported here:

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Array.2Efoldl.20bug.20.28can.20prove.20False.29/near/565077432
2025-12-22 23:00:16 +00:00
..
Lex feat: more Nat range lemmas (#11321) 2025-12-04 14:14:45 +00:00
QSort feat: integrate high-level order typeclasses with BEq and Ord (#9908) 2025-08-19 07:54:53 +00:00
Subarray chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Attach.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
Basic.lean fix: Array.foldlMUnsafe bug (#11772) 2025-12-22 23:00:16 +00:00
BasicAux.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
BinSearch.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Bootstrap.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
Count.lean chore: remove @[grind =] from List.countP_eq_length_filter (#11542) 2025-12-08 03:11:25 +00:00
DecidableEq.lean chore: post-stage0 update fixes 2025-12-10 17:28:06 +01:00
Erase.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
Extract.lean feat: allow decidable equality for empty lists and empty arrays (#11269) 2025-11-20 20:19:31 +00:00
Find.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
FinRange.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
GetLit.lean chore: add deprecations for duplicated theorems (#10967) 2025-10-29 05:26:16 +00:00
InsertIdx.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
InsertionSort.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Lemmas.lean feat: add guarded grind_pattern to List.eq_nil_of_length_eq_zero (#11760) 2025-12-22 00:05:58 +00:00
Lex.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
MapIdx.lean chore: remove >6 month old deprecations (#10968) 2025-10-26 10:01:30 +00:00
Mem.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Monadic.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00
OfFn.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Perm.lean chore: add deprecations for duplicated theorems (#10967) 2025-10-29 05:26:16 +00:00
QSort.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Range.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Set.lean feat: make private the default in module (#9044) 2025-06-28 16:30:53 +00:00
Subarray.lean feat: @[suggest_for] annotations for prompting easy-to-miss names (#11554) 2025-12-10 22:50:45 +00:00
TakeDrop.lean chore: remove redundant imports in core (#10750) 2025-10-16 20:27:46 +00:00
Zip.lean chore: remove ≥6 month old deprecations (#11627) 2025-12-12 10:40:04 +00:00