Commit 2025-03-10 10:24 a19bd4cf
View on Github →feat(Data/Seq): structural lemmas (#19859)
- Add several theorems about
Stream'.Seq
, mainly on sequence operations withnil
andcons
. - Introduce the
fold
operation for sequences and prove a few structural lemmas about it. - Rename
Seq.destruct_eq_nil
asSeq.destruct_eq_none
.