commit: e7bd8082350fe9e655a0223732f6b90a0c4aa80e

[log]
author: Paul Reichert <6992158+datokrat@users.noreply.github.com>

Fri Jun 13 10:32:18 2025 +0200
committer: Paul Reichert <6992158+datokrat@users.noreply.github.com>

Fri Jun 13 10:32:18 2025 +0200
tree: d06354fd791d203cdd9418e5bfc01a33f2d1afe7
parent: ee486182e16a1952a32236c4d6b968520f6bc848 [diff]

wip: move consumer lemmas to Init

src/Init/Data/Iterators.lean[diff]
src/Init/Data/Iterators/Lemmas.lean[Added - diff]
src/Init/Data/Iterators/Lemmas/Consumers.lean[Added - diff]
src/Init/Data/Iterators/Lemmas/Consumers/Collect.lean[Renamed from src/Std/Data/Iterators/Lemmas/Consumers/Collect.lean - diff]
src/Init/Data/Iterators/Lemmas/Consumers/Loop.lean[Renamed from src/Std/Data/Iterators/Lemmas/Consumers/Loop.lean - diff]
src/Init/Data/Iterators/Lemmas/Consumers/Monadic.lean[Added - diff]
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean[Renamed from src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Collect.lean - diff]
src/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean[Renamed from src/Std/Data/Iterators/Lemmas/Consumers/Monadic/Loop.lean - diff]
src/Init/Data/List/Range.lean[diff]
src/Init/Data/Range/Classes.lean[Added - diff]
src/Init/Data/Range/New/Basic.lean[diff]
src/Init/Data/Range/New/Classes.lean[Deleted - diff]
src/Init/Data/Range/New/Lemmas.lean[diff]
src/Init/Data/Range/New/Nat.lean[diff]
src/Init/Data/Range/New/RangeIterator.lean[diff]
src/Std/Data/Iterators/Lemmas.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Drop.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/DropWhile.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/FilterMap.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Drop.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/DropWhile.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/FilterMap.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Take.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/TakeWhile.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Monadic/Zip.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Take.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/TakeWhile.lean[diff]
src/Std/Data/Iterators/Lemmas/Combinators/Zip.lean[diff]
src/Std/Data/Iterators/Lemmas/Consumers.lean[diff]
src/Std/Data/Iterators/Lemmas/Consumers/Monadic.lean[Deleted - diff]
src/Std/Data/Iterators/Lemmas/Producers/Array.lean[diff]
src/Std/Data/Iterators/Lemmas/Producers/Empty.lean[diff]
src/Std/Data/Iterators/Lemmas/Producers/List.lean[diff]
src/Std/Data/Iterators/Lemmas/Producers/Monadic/Array.lean[diff]
src/Std/Data/Iterators/Lemmas/Producers/Monadic/Empty.lean[diff]
src/Std/Data/Iterators/Lemmas/Producers/Monadic/List.lean[diff]

36 files changed

tree: d06354fd791d203cdd9418e5bfc01a33f2d1afe7

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean.