Skip to content

Commit 1d5cff9

Browse files
vasnesterovBjorn Wehlin
authored andcommitted
refactor(Data/Seq): reorganize Seq.lean (leanprover-community#20071)
The `Seq` API in the `Seq.lean` file was somewhat disorganized. This PR reorganizes the file to make it more structured. It arranges the API in the following way: 1. Definitions and the `get?` function. 2. Constructors: `nil` and `cons`. 3. Destructors: `head`, `tail`, and `destruct`. 4. Recursion and corecursion principles. 5. Bisimulation. 6. `Terminates` API. 7. `Membership` for sequences. 8. Conversion to and from other types (`List`, `Stream`, `MLList`) and `take` operation as it is required for conversion to `List`. 9. Definitions of other operations on sequences (`append`, `map`, `join`, etc.). 10. Lemmas about conversions and operations, organized into sections by the primary operation of each lemma.
1 parent 10d5813 commit 1d5cff9

3 files changed

Lines changed: 502 additions & 441 deletions

File tree

0 commit comments

Comments
 (0)