lean4-htt/src/Std
Paul Reichert 274997420a
refactor: remove backward compatibility options from iterator/slice/range modules (#12925)
This PR removes `respectTransparency`, `reducibleClassField` and `simp
+instances` usages in the iterator/slice/range modules.
2026-03-15 14:03:51 +00:00
..
Data refactor: remove backward compatibility options from iterator/slice/range modules (#12925) 2026-03-15 14:03:51 +00:00
Do feat: add withEarlyReturnNewDo variants for new do elaborator (#12881) 2026-03-11 10:44:34 +00:00
Internal fix: remove use of native_decide in the HTTP library (#12857) 2026-03-10 13:25:22 +00:00
Net refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Sat perf: remove the additional relabeling step during AIG to CNF conversion (#12480) 2026-02-14 17:08:07 +00:00
Sync chore: shake core (#12276) 2026-02-05 09:10:32 +00:00
Tactic feat: add @[mvcgen_witness_type] attribute for extensible witness classification (#12882) 2026-03-11 11:38:05 +00:00
Time feat: backward.isDefEq.respectTransparency (#12179) 2026-02-16 15:57:21 +00:00
Data.lean feat: add decidable equality to DHashMap/HashMap/HashSet and their extensional variants (#11421) 2025-12-12 09:55:55 +00:00
Do.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Internal.lean feat: add core HTTP data types (#12126) 2026-03-04 14:32:29 +00:00
Net.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Sat.lean chore: remove public section from end of files (#10684) 2025-10-06 13:30:48 +00:00
Sync.lean feat: introduce CancellationContext type for cancellation with context propagation (#11499) 2025-12-15 21:20:11 +00:00
Tactic.lean refactor: module-ize remainder of Std (#9195) 2025-07-17 11:43:57 +00:00
Time.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00