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 with nil and cons.
  • Introduce the fold operation for sequences and prove a few structural lemmas about it.
  • Rename Seq.destruct_eq_nil as Seq.destruct_eq_none.

Estimated changes

added theorem Stream'.Seq.corec_cons
added theorem Stream'.Seq.corec_nil
added theorem Stream'.Seq.drop_get?
added theorem Stream'.Seq.drop_nil
added def Stream'.Seq.fold
added theorem Stream'.Seq.fold_cons
added theorem Stream'.Seq.fold_head
added theorem Stream'.Seq.fold_nil
added theorem Stream'.Seq.get?_mem
added theorem Stream'.Seq.take_drop
added theorem Stream'.Seq.take_nil
added theorem Stream'.Seq.take_zero
added theorem Stream'.Seq.val_eq_get
added theorem Stream'.Seq.zip_map