lean4-htt/src/Init/Data/Iterators
Paul Reichert 16919852d9
refactor: remove last appearances of allowNontermination (#12211)
This PR updates docstrings and function signatures in order to complete
the transition from `Iter.Partial` to `Iter.Total` (extrinsically
terminating by default). It also deprecates `allowNontermination` and
adds `Iter.Total.atIdxSlow?`.
2026-01-29 07:22:19 +00:00
..
Combinators feat: make FinitenessRelation part of the public API (#11789) 2025-12-29 20:45:41 +00:00
Consumers refactor: remove last appearances of allowNontermination (#12211) 2026-01-29 07:22:19 +00:00
Internal feat: Std.Iter.first? (#12162) 2026-01-27 12:10:16 +00:00
Lemmas refactor: remove last appearances of allowNontermination (#12211) 2026-01-29 07:22:19 +00:00
Producers feat: make FinitenessRelation part of the public API (#11789) 2025-12-29 20:45:41 +00:00
Basic.lean refactor: remove last appearances of allowNontermination (#12211) 2026-01-29 07:22:19 +00:00
Combinators.lean feat: List slices (#11019) 2025-11-14 11:33:25 +00:00
Consumers.lean feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038) 2025-12-08 16:03:22 +00:00
Internal.lean feat: make FinitenessRelation part of the public API (#11789) 2025-12-29 20:45:41 +00:00
Lemmas.lean feat: List slices (#11019) 2025-11-14 11:33:25 +00:00
PostconditionMonad.lean style: fix typos in Init/ and Std/ docstrings (#11864) 2026-01-09 07:24:07 +00:00
Producers.lean feat: List slices (#11019) 2025-11-14 11:33:25 +00:00
ToIterator.lean refactor: move Iter and others from Std.Iterators to Std (#11446) 2025-12-15 08:24:12 +00:00