Skip to content

Conversation

ctchou
Copy link

@ctchou ctchou commented Oct 7, 2025

In the previous PR #80, ωList is just a copy of Stream' with suitable name changes. Now we make three major modifications:

  1. We make it clear that ωList α is really an abstraction of ℕ → α. In particular, for s : ωList and n : ℕ, the n-th elements of s is now obtained by s n, not s.get n or get s n. Indeed, we have got rid of the API function get altogether.
  2. The infix notation for appendωList is changed from++ₛ to ++ₗ (the last letter is a lowercase "L" subscript). This is to avoid conflict with Stream'.
  3. A new API function extract, which is the analogue of List.extract, and a number of theorems involving it are added.

@ctchou
Copy link
Author

ctchou commented Oct 7, 2025

Rebase on the current "main".

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant