Commit 2025-05-12 18:43 0b8dda7d
View on Github →refactor(Data/Seq): reorganize Seq.lean (#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:
- Definitions and the
get?function. - Constructors:
nilandcons. - Destructors:
head,tail, anddestruct. - Recursion and corecursion principles.
- Bisimulation.
TerminatesAPI.Membershipfor sequences.- Conversion to and from other types (
List,Stream,MLList) andtakeoperation as it is required for conversion toList. - Definitions of other operations on sequences (
append,map,join, etc.). - Lemmas about conversions and operations, organized into sections by the primary operation of each lemma.