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:
nil
andcons
. - Destructors:
head
,tail
, anddestruct
. - Recursion and corecursion principles.
- Bisimulation.
Terminates
API.Membership
for sequences.- Conversion to and from other types (
List
,Stream
,MLList
) andtake
operation 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.