Commit 2025-08-29 19:57 1b37a9ae

View on Github →

chore(Data/Seq): split Seq.lean (#28954) Split Data/Seq/Basic.lean into Defs.lean and Basic.lean.

Estimated changes

deleted def Stream'.IsSeq
deleted def Stream'.Seq.BisimO
deleted def Stream'.Seq.Corec.f
deleted def Stream'.Seq.append
deleted theorem Stream'.Seq.coinduction2
deleted theorem Stream'.Seq.coinduction
deleted def Stream'.Seq.cons
deleted theorem Stream'.Seq.cons_eq_cons
deleted theorem Stream'.Seq.cons_ne_nil
deleted def Stream'.Seq.corec
deleted theorem Stream'.Seq.corec_cons
deleted theorem Stream'.Seq.corec_eq
deleted theorem Stream'.Seq.corec_nil
deleted theorem Stream'.Seq.destruct_cons
deleted theorem Stream'.Seq.destruct_nil
deleted def Stream'.Seq.drop
deleted def Stream'.Seq.enum
deleted theorem Stream'.Seq.eq_of_bisim
deleted def Stream'.Seq.fold
deleted theorem Stream'.Seq.ge_stable
deleted def Stream'.Seq.get?
deleted theorem Stream'.Seq.get?_mem
deleted theorem Stream'.Seq.get?_mk
deleted theorem Stream'.Seq.get?_nil
deleted theorem Stream'.Seq.get?_tail
deleted def Stream'.Seq.head
deleted theorem Stream'.Seq.head_cons
deleted theorem Stream'.Seq.head_eq_none
deleted theorem Stream'.Seq.head_eq_some
deleted theorem Stream'.Seq.head_nil
deleted def Stream'.Seq.join
deleted theorem Stream'.Seq.le_stable
deleted def Stream'.Seq.length
deleted theorem Stream'.Seq.length_le_iff
deleted theorem Stream'.Seq.length_nil
deleted theorem Stream'.Seq.lt_length_iff
deleted def Stream'.Seq.map
deleted theorem Stream'.Seq.mem_cons
deleted theorem Stream'.Seq.mem_cons_iff
deleted theorem Stream'.Seq.mem_rec_on
deleted def Stream'.Seq.nats
deleted def Stream'.Seq.nil
deleted theorem Stream'.Seq.nil_ne_cons
deleted theorem Stream'.Seq.notMem_nil
deleted def Stream'.Seq.ofList
deleted theorem Stream'.Seq.ofList_cons
deleted theorem Stream'.Seq.ofList_get?
deleted theorem Stream'.Seq.ofList_nil
deleted def Stream'.Seq.omap
deleted def Stream'.Seq.recOn
deleted def Stream'.Seq.set
deleted def Stream'.Seq.splitAt
deleted def Stream'.Seq.tail
deleted theorem Stream'.Seq.tail_cons
deleted theorem Stream'.Seq.tail_nil
deleted def Stream'.Seq.take
deleted def Stream'.Seq.toList'
deleted def Stream'.Seq.toList
deleted def Stream'.Seq.unzip
deleted def Stream'.Seq.update
deleted theorem Stream'.Seq.val_cons
deleted theorem Stream'.Seq.val_eq_get
deleted def Stream'.Seq.zip
deleted def Stream'.Seq.zipWith
deleted def Stream'.Seq1
deleted def Stream'.Seq
added def Stream'.IsSeq
added def Stream'.Seq.cons
added theorem Stream'.Seq.corec_cons
added theorem Stream'.Seq.corec_eq
added theorem Stream'.Seq.corec_nil
added def Stream'.Seq.drop
added def Stream'.Seq.enum
added def Stream'.Seq.fold
added theorem Stream'.Seq.ge_stable
added def Stream'.Seq.get?
added theorem Stream'.Seq.get?_mem
added theorem Stream'.Seq.get?_mk
added theorem Stream'.Seq.get?_nil
added theorem Stream'.Seq.get?_tail
added def Stream'.Seq.head
added theorem Stream'.Seq.head_cons
added theorem Stream'.Seq.head_nil
added def Stream'.Seq.join
added theorem Stream'.Seq.le_stable
added theorem Stream'.Seq.length_nil
added def Stream'.Seq.map
added theorem Stream'.Seq.mem_cons
added theorem Stream'.Seq.mem_rec_on
added def Stream'.Seq.nats
added def Stream'.Seq.nil
added theorem Stream'.Seq.notMem_nil
added theorem Stream'.Seq.ofList_nil
added def Stream'.Seq.omap
added def Stream'.Seq.set
added def Stream'.Seq.tail
added theorem Stream'.Seq.tail_cons
added theorem Stream'.Seq.tail_nil
added def Stream'.Seq.take
added theorem Stream'.Seq.val_cons
added theorem Stream'.Seq.val_eq_get
added def Stream'.Seq.zip
added def Stream'.Seq1
added def Stream'.Seq