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:

  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.

Estimated changes