Documentation

Mathlib.Data.Seq.Seq

Possibly infinite lists #

This file provides a Seq α type representing possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

def Stream'.IsSeq {α : Type u} (s : Stream' (Option α)) :

A stream s : Option α is a sequence if s.get n = none implies s.get (n + 1) = none.

Equations
def Stream'.Seq (α : Type u) :

Seq α is the type of possibly infinite lists (referred here as sequences). It is encoded as an infinite stream of options such that if f n = none, then f m = none for all m ≥ n.

Equations
def Stream'.Seq1 (α : Type u_1) :
Type u_1

Seq1 α is the type of nonempty sequences.

Equations
def Stream'.Seq.get? {α : Type u} :
Seq αOption α

Get the nth element of a sequence (if it exists)

Equations
@[simp]
theorem Stream'.Seq.val_eq_get {α : Type u} (s : Seq α) (n : ) :
s n = s.get? n
@[simp]
theorem Stream'.Seq.get?_mk {α : Type u} (f : Stream' (Option α)) (hf : f.IsSeq) :
get? f, hf = f
theorem Stream'.Seq.le_stable {α : Type u} (s : Seq α) {m n : } (h : m n) :
s.get? m = nones.get? n = none
theorem Stream'.Seq.ge_stable {α : Type u} (s : Seq α) {aₙ : α} {n m : } (m_le_n : m n) (s_nth_eq_some : s.get? n = some aₙ) :
(aₘ : α), s.get? m = some aₘ

If s.get? n = some aₙ for some value aₙ, then there is also some value aₘ such that s.get? = some aₘ for m ≤ n.

theorem Stream'.Seq.ext {α : Type u} {s t : Seq α} (h : ∀ (n : ), s.get? n = t.get? n) :
s = t
theorem Stream'.Seq.ext_iff {α : Type u} {s t : Seq α} :
s = t ∀ (n : ), s.get? n = t.get? n

Constructors #

def Stream'.Seq.nil {α : Type u} :
Seq α

The empty sequence

Equations
def Stream'.Seq.cons {α : Type u} (a : α) (s : Seq α) :
Seq α

Prepend an element to a sequence

Equations
@[simp]
theorem Stream'.Seq.val_cons {α : Type u} (s : Seq α) (x : α) :
(cons x s) = Stream'.cons (some x) s
@[simp]
theorem Stream'.Seq.get?_nil {α : Type u} (n : ) :
@[simp]
theorem Stream'.Seq.get?_zero_eq_none {α : Type u} {s : Seq α} :
s.get? 0 = none s = nil
@[simp]
theorem Stream'.Seq.get?_cons_zero {α : Type u} (a : α) (s : Seq α) :
(cons a s).get? 0 = some a
@[simp]
theorem Stream'.Seq.get?_cons_succ {α : Type u} (a : α) (s : Seq α) (n : ) :
(cons a s).get? (n + 1) = s.get? n
@[simp]
theorem Stream'.Seq.cons_ne_nil {α : Type u} {x : α} {s : Seq α} :
@[simp]
theorem Stream'.Seq.nil_ne_cons {α : Type u} {x : α} {s : Seq α} :
theorem Stream'.Seq.cons_left_injective {α : Type u} (s : Seq α) :
Function.Injective fun (x : α) => cons x s
theorem Stream'.Seq.cons_eq_cons {α : Type u} {x x' : α} {s s' : Seq α} :
cons x s = cons x' s' x = x' s = s'

Destructors #

def Stream'.Seq.head {α : Type u} (s : Seq α) :

Get the first element of a sequence

Equations
def Stream'.Seq.tail {α : Type u} (s : Seq α) :
Seq α

Get the tail of a sequence (or nil if the sequence is nil)

Equations
def Stream'.Seq.destruct {α : Type u} (s : Seq α) :

Destructor for a sequence, resulting in either none (for nil) or some (a, s) (for cons a s).

Equations
@[simp]
theorem Stream'.Seq.get?_tail {α : Type u} (s : Seq α) (n : ) :
s.tail.get? n = s.get? (n + 1)
@[simp]
theorem Stream'.Seq.destruct_cons {α : Type u} (a : α) (s : Seq α) :
theorem Stream'.Seq.destruct_eq_none {α : Type u} {s : Seq α} :
s.destruct = nones = nil
theorem Stream'.Seq.destruct_eq_cons {α : Type u} {s : Seq α} {a : α} {s' : Seq α} :
s.destruct = some (a, s')s = cons a s'
@[simp]
@[simp]
theorem Stream'.Seq.head_cons {α : Type u} (a : α) (s : Seq α) :
(cons a s).head = some a
@[simp]
@[simp]
theorem Stream'.Seq.tail_cons {α : Type u} (a : α) (s : Seq α) :
(cons a s).tail = s
theorem Stream'.Seq.head_eq_some {α : Type u} {s : Seq α} {x : α} (h : s.head = some x) :
s = cons x s.tail
theorem Stream'.Seq.head_eq_none {α : Type u} {s : Seq α} (h : s.head = none) :
s = nil
@[simp]
theorem Stream'.Seq.head_eq_none_iff {α : Type u} {s : Seq α} :

Recursion and corecursion principles #

def Stream'.Seq.recOn {α : Type u} {motive : Seq αSort v} (s : Seq α) (nil : motive nil) (cons : (x : α) → (s : Seq α) → motive (cons x s)) :
motive s

Recursion principle for sequences, compare with List.recOn.

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.Seq.omap {α : Type u} {β : Type v} {γ : Type w} (f : βγ) :
Option (α × β)Option (α × γ)

Functorial action of the functor Option (α × _)

Equations
def Stream'.Seq.Corec.f {α : Type u} {β : Type v} (f : βOption (α × β)) :
Option βOption α × Option β

Corecursor over pairs of Option values

Equations
def Stream'.Seq.corec {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :
Seq α

Corecursor for Seq α as a coinductive type. Iterates f to produce new elements of the sequence until none is obtained.

Equations
@[simp]
theorem Stream'.Seq.corec_eq {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) :
(corec f b).destruct = omap (corec f) (f b)
theorem Stream'.Seq.corec_nil {α : Type u} {β : Type v} (f : βOption (α × β)) (b : β) (h : f b = none) :
corec f b = nil
theorem Stream'.Seq.corec_cons {α : Type u} {β : Type v} {f : βOption (α × β)} {b : β} {x : α} {s : β} (h : f b = some (x, s)) :
corec f b = cons x (corec f s)

Bisimulation #

def Stream'.Seq.BisimO {α : Type u} (R : Seq αSeq αProp) :
Option (Seq1 α)Option (Seq1 α)Prop

Bisimilarity relation over Option of Seq1 α

Equations
def Stream'.Seq.IsBisimulation {α : Type u} (R : Seq αSeq αProp) :

a relation is bisimilar if it meets the BisimO test

Equations
theorem Stream'.Seq.eq_of_bisim {α : Type u} (R : Seq αSeq αProp) (bisim : IsBisimulation R) {s₁ s₂ : Seq α} (r : R s₁ s₂) :
s₁ = s₂
theorem Stream'.Seq.coinduction {α : Type u} {s₁ s₂ : Seq α} :
s₁.head = s₂.head(∀ (β : Type u) (fr : Seq αβ), fr s₁ = fr s₂fr s₁.tail = fr s₂.tail)s₁ = s₂
theorem Stream'.Seq.coinduction2 {α : Type u} {β : Type v} (s : Seq α) (f g : Seq αSeq β) (H : ∀ (s : Seq α), BisimO (fun (s1 s2 : Seq β) => (s : Seq α), s1 = f s s2 = g s) (f s).destruct (g s).destruct) :
f s = g s

Termination #

def Stream'.Seq.TerminatedAt {α : Type u} (s : Seq α) (n : ) :

A sequence has terminated at position n if the value at position n equals none.

Equations
instance Stream'.Seq.terminatedAtDecidable {α : Type u} (s : Seq α) (n : ) :

It is decidable whether a sequence terminates at a given position.

Equations
def Stream'.Seq.Terminates {α : Type u} (s : Seq α) :

A sequence terminates if there is some position n at which it has terminated.

Equations
def Stream'.Seq.length {α : Type u} (s : Seq α) (h : s.Terminates) :

The length of a terminating sequence.

Equations
theorem Stream'.Seq.terminated_stable {α : Type u} (s : Seq α) {m n : } :
m ns.TerminatedAt ms.TerminatedAt n

If a sequence terminated at position n, it also terminated at m ≥ n.

theorem Stream'.Seq.not_terminates_iff {α : Type u} {s : Seq α} :
¬s.Terminates ∀ (n : ), (s.get? n).isSome = true
@[simp]
@[simp]
theorem Stream'.Seq.cons_not_terminatedAt_zero {α : Type u} {x : α} {s : Seq α} :
@[simp]
theorem Stream'.Seq.cons_terminatedAt_succ_iff {α : Type u} {x : α} {s : Seq α} {n : } :
@[simp]
theorem Stream'.Seq.terminates_cons_iff {α : Type u} {x : α} {s : Seq α} :
@[simp]
theorem Stream'.Seq.length_nil {α : Type u} :
nil.length = 0
@[simp]
theorem Stream'.Seq.length_eq_zero {α : Type u} {s : Seq α} {h : s.Terminates} :
s.length h = 0 s = nil
theorem Stream'.Seq.length_le_iff' {α : Type u} {s : Seq α} {n : } :

The statement of length_le_iff' does not assume that the sequence terminates. For a simpler statement of the theorem where the sequence is known to terminate see length_le_iff

theorem Stream'.Seq.length_le_iff {α : Type u} {s : Seq α} {n : } {h : s.Terminates} :

The statement of length_le_iff assumes that the sequence terminates. For a statement of the where the sequence is not known to terminate see length_le_iff'

theorem Stream'.Seq.lt_length_iff' {α : Type u} {s : Seq α} {n : } :
(∀ (h : s.Terminates), n < s.length h) (a : α), a s.get? n

The statement of lt_length_iff' does not assume that the sequence terminates. For a simpler statement of the theorem where the sequence is known to terminate see lt_length_iff

theorem Stream'.Seq.lt_length_iff {α : Type u} {s : Seq α} {n : } {h : s.Terminates} :
n < s.length h (a : α), a s.get? n

The statement of length_le_iff assumes that the sequence terminates. For a statement of the where the sequence is not known to terminate see length_le_iff'

Membership #

def Stream'.Seq.Mem {α : Type u} (s : Seq α) (a : α) :

member definition for Seq

Equations
@[simp]
theorem Stream'.Seq.get?_mem {α : Type u} {s : Seq α} {n : } {x : α} (h : s.get? n = some x) :
x s
theorem Stream'.Seq.notMem_nil {α : Type u} (a : α) :
@[deprecated Stream'.Seq.notMem_nil (since := "2025-05-23")]
theorem Stream'.Seq.not_mem_nil {α : Type u} (a : α) :

Alias of Stream'.Seq.notMem_nil.

theorem Stream'.Seq.mem_cons {α : Type u} (a : α) (s : Seq α) :
a cons a s
theorem Stream'.Seq.mem_cons_of_mem {α : Type u} (y : α) {a : α} {s : Seq α} :
a sa cons y s
theorem Stream'.Seq.eq_or_mem_of_mem_cons {α : Type u} {a b : α} {s : Seq α} :
a cons b sa = b a s
@[simp]
theorem Stream'.Seq.mem_cons_iff {α : Type u} {a b : α} {s : Seq α} :
a cons b s a = b a s
theorem Stream'.Seq.mem_rec_on {α : Type u} {C : Seq αProp} {a : α} {s : Seq α} (M : a s) (h1 : ∀ (b : α) (s' : Seq α), a = b C s'C (cons b s')) :
C s

Converting from/to other types #

def Stream'.Seq.ofList {α : Type u} (l : List α) :
Seq α

Embed a list as a sequence

Equations
instance Stream'.Seq.coeList {α : Type u} :
Coe (List α) (Seq α)
Equations
@[simp]
theorem Stream'.Seq.ofList_nil {α : Type u} :
[] = nil
@[simp]
theorem Stream'.Seq.ofList_get? {α : Type u} (l : List α) (n : ) :
(↑l).get? n = l[n]?
@[deprecated Stream'.Seq.ofList_get? (since := "2025-02-21")]
theorem Stream'.Seq.ofList_get {α : Type u} (l : List α) (n : ) :
(↑l).get? n = l[n]?

Alias of Stream'.Seq.ofList_get?.

@[simp]
theorem Stream'.Seq.ofList_cons {α : Type u} (a : α) (l : List α) :
↑(a :: l) = cons a l
def Stream'.Seq.ofStream {α : Type u} (s : Stream' α) :
Seq α

Embed an infinite stream as a sequence

Equations
def Stream'.Seq.ofMLList {α : Type u} :
MLList Id αSeq α

Embed a MLList α as a sequence. Note that even though this is non-meta, it will produce infinite sequences if used with cyclic MLLists created by meta constructions.

Equations
unsafe def Stream'.Seq.toMLList {α : Type u} :
Seq αMLList Id α

Translate a sequence into a MLList.

Equations
unsafe def Stream'.Seq.forceToList {α : Type u} (s : Seq α) :
List α

Translate a sequence to a list. This function will run forever if run on an infinite sequence.

Equations
def Stream'.Seq.take {α : Type u} :
Seq αList α

Take the first n elements of the sequence (producing a list)

Equations
def Stream'.Seq.toList {α : Type u} (s : Seq α) (h : s.Terminates) :
List α

Convert a sequence which is known to terminate into a list

Equations
def Stream'.Seq.toStream {α : Type u} (s : Seq α) (h : ¬s.Terminates) :

Convert a sequence which is known not to terminate into a stream

Equations

Convert a sequence into either a list or a stream depending on whether it is finite or infinite. (Without decidability of the infiniteness predicate, this is not constructively possible.)

Equations
def Stream'.Seq.toList' {α : Type u_1} (s : Seq α) :

Convert a sequence into a list, embedded in a computation to allow for the possibility of infinite sequences (in which case the computation never returns anything).

Equations
  • One or more equations did not get rendered due to their size.

Operations on sequences #

def Stream'.Seq.append {α : Type u} (s₁ s₂ : Seq α) :
Seq α

Append two sequences. If s₁ is infinite, then s₁ ++ s₂ = s₁, otherwise it puts s₂ at the location of the nil in s₁.

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.Seq.map {α : Type u} {β : Type v} (f : αβ) :
Seq αSeq β

Map a function over a sequence.

Equations
def Stream'.Seq.join {α : Type u} :
Seq (Seq1 α)Seq α

Flatten a sequence of sequences. (It is required that the sequences be nonempty to ensure productivity; in the case of an infinite sequence of nil, the first element is never generated.)

Equations
  • One or more equations did not get rendered due to their size.
def Stream'.Seq.drop {α : Type u} (s : Seq α) :
Seq α

Remove the first n elements from the sequence.

Equations
def Stream'.Seq.splitAt {α : Type u} :
Seq αList α × Seq α

Split a sequence at n, producing a finite initial segment and an infinite tail.

Equations
def Stream'.Seq.zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s₁ : Seq α) (s₂ : Seq β) :
Seq γ

Combine two sequences with a function

Equations
def Stream'.Seq.zip {α : Type u} {β : Type v} :
Seq αSeq βSeq (α × β)

Pair two sequences into a sequence of pairs

Equations
def Stream'.Seq.unzip {α : Type u} {β : Type v} (s : Seq (α × β)) :
Seq α × Seq β

Separate a sequence of pairs into two sequences

Equations

The sequence of natural numbers some 0, some 1, ...

Equations
def Stream'.Seq.enum {α : Type u} (s : Seq α) :
Seq ( × α)

Enumerate a sequence by tagging each element with its index.

Equations
def Stream'.Seq.fold {α : Type u} {β : Type v} (s : Seq α) (init : β) (f : βαβ) :
Seq β

Folds a sequence using f, producing a sequence of intermediate values, i.e. [init, f init s.head, f (f init s.head) s.tail.head, ...].

Equations
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Stream'.Seq.ofStream_cons {α : Type u} (a : α) (s : Stream' α) :
(Stream'.cons a s) = cons a s
theorem Stream'.Seq.terminates_ofList {α : Type u} (l : List α) :
(↑l).Terminates
@[simp]
theorem Stream'.Seq.take_nil {α : Type u} {n : } :
@[simp]
theorem Stream'.Seq.take_zero {α : Type u} {s : Seq α} :
take 0 s = []
@[simp]
theorem Stream'.Seq.take_succ_cons {α : Type u} {n : } {x : α} {s : Seq α} :
take (n + 1) (cons x s) = x :: take n s
@[simp]
theorem Stream'.Seq.getElem?_take {α : Type u} (n k : ) (s : Seq α) :
(take k s)[n]? = if n < k then s.get? n else none
theorem Stream'.Seq.get?_mem_take {α : Type u} {s : Seq α} {m n : } (h_mn : m < n) {x : α} (h_get : s.get? m = some x) :
x take n s
theorem Stream'.Seq.length_take_le {α : Type u} {s : Seq α} {n : } :
(take n s).length n
theorem Stream'.Seq.length_take_of_le_length {α : Type u} {s : Seq α} {n : } (hle : ∀ (h : s.Terminates), n s.length h) :
(take n s).length = n
@[simp]
theorem Stream'.Seq.length_toList {α : Type u} (s : Seq α) (h : s.Terminates) :
(s.toList h).length = s.length h
@[simp]
theorem Stream'.Seq.getElem?_toList {α : Type u} (s : Seq α) (h : s.Terminates) (n : ) :
(s.toList h)[n]? = s.get? n
@[simp]
theorem Stream'.Seq.ofList_toList {α : Type u} (s : Seq α) (h : s.Terminates) :
(s.toList h) = s
@[simp]
theorem Stream'.Seq.toList_ofList {α : Type u} (l : List α) :
(↑l).toList = l
@[simp]
theorem Stream'.Seq.toList_nil {α : Type u} :
theorem Stream'.Seq.getLast?_toList {α : Type u} (s : Seq α) (h : s.Terminates) :
(s.toList h).getLast? = s.get? (s.length h - 1)
@[simp]
theorem Stream'.Seq.cons_append {α : Type u} (a : α) (s t : Seq α) :
(cons a s).append t = cons a (s.append t)
@[simp]
theorem Stream'.Seq.nil_append {α : Type u} (s : Seq α) :
@[simp]
theorem Stream'.Seq.append_nil {α : Type u} (s : Seq α) :
@[simp]
theorem Stream'.Seq.append_assoc {α : Type u} (s t u : Seq α) :
(s.append t).append u = s.append (t.append u)
theorem Stream'.Seq.of_mem_append {α : Type u} {s₁ s₂ : Seq α} {a : α} (h : a s₁.append s₂) :
a s₁ a s₂
theorem Stream'.Seq.mem_append_left {α : Type u} {s₁ s₂ : Seq α} {a : α} (h : a s₁) :
a s₁.append s₂
@[simp]
theorem Stream'.Seq.ofList_append {α : Type u} (l l' : List α) :
↑(l ++ l') = (↑l).append l'
@[simp]
theorem Stream'.Seq.ofStream_append {α : Type u} (l : List α) (s : Stream' α) :
↑(l ++ₛ s) = (↑l).append s
@[simp]
theorem Stream'.Seq.map_get? {α : Type u} {β : Type v} (f : αβ) (s : Seq α) (n : ) :
(map f s).get? n = Option.map f (s.get? n)
@[simp]
theorem Stream'.Seq.map_nil {α : Type u} {β : Type v} (f : αβ) :
@[simp]
theorem Stream'.Seq.map_cons {α : Type u} {β : Type v} (f : αβ) (a : α) (s : Seq α) :
map f (cons a s) = cons (f a) (map f s)
@[simp]
theorem Stream'.Seq.map_id {α : Type u} (s : Seq α) :
map id s = s
@[simp]
theorem Stream'.Seq.map_tail {α : Type u} {β : Type v} (f : αβ) (s : Seq α) :
map f s.tail = (map f s).tail
theorem Stream'.Seq.map_comp {α : Type u} {β : Type v} {γ : Type w} (f : αβ) (g : βγ) (s : Seq α) :
map (g f) s = map g (map f s)
@[simp]
theorem Stream'.Seq.terminatedAt_map_iff {α : Type u} {β : Type v} {f : αβ} {s : Seq α} {n : } :
@[simp]
theorem Stream'.Seq.terminates_map_iff {α : Type u} {β : Type v} {f : αβ} {s : Seq α} :
@[simp]
theorem Stream'.Seq.length_map {α : Type u} {β : Type v} {s : Seq α} {f : αβ} (h : (map f s).Terminates) :
(map f s).length h = s.length
theorem Stream'.Seq.mem_map {α : Type u} {β : Type v} (f : αβ) {a : α} {s : Seq α} :
a sf a map f s
theorem Stream'.Seq.exists_of_mem_map {α : Type u} {β : Type v} {f : αβ} {b : β} {s : Seq α} :
b map f s (a : α), a s f a = b
@[simp]
theorem Stream'.Seq.map_append {α : Type u} {β : Type v} (f : αβ) (s t : Seq α) :
map f (s.append t) = (map f s).append (map f t)
@[simp]
theorem Stream'.Seq.join_cons_nil {α : Type u} (a : α) (S : Seq (Seq1 α)) :
theorem Stream'.Seq.join_cons_cons {α : Type u} (a b : α) (s : Seq α) (S : Seq (Seq1 α)) :
(cons (a, cons b s) S).join = cons a (cons (b, s) S).join
@[simp]
theorem Stream'.Seq.join_cons {α : Type u} (a : α) (s : Seq α) (S : Seq (Seq1 α)) :
(cons (a, s) S).join = cons a (s.append S.join)
@[simp]
theorem Stream'.Seq.join_append {α : Type u} (S T : Seq (Seq1 α)) :
@[simp]
theorem Stream'.Seq.drop_get? {α : Type u} {n m : } {s : Seq α} :
(s.drop n).get? m = s.get? (n + m)
theorem Stream'.Seq.dropn_add {α : Type u} (s : Seq α) (m n : ) :
s.drop (m + n) = (s.drop m).drop n
theorem Stream'.Seq.dropn_tail {α : Type u} (s : Seq α) (n : ) :
s.tail.drop n = s.drop (n + 1)
@[simp]
theorem Stream'.Seq.head_dropn {α : Type u} (s : Seq α) (n : ) :
(s.drop n).head = s.get? n
@[simp]
theorem Stream'.Seq.drop_succ_cons {α : Type u} {x : α} {s : Seq α} {n : } :
(cons x s).drop (n + 1) = s.drop n
@[simp]
theorem Stream'.Seq.drop_nil {α : Type u} {n : } :
theorem Stream'.Seq.take_drop {α : Type u} {s : Seq α} {n m : } :
List.drop m (take n s) = take (n - m) (s.drop m)
@[simp]
theorem Stream'.Seq.get?_zipWith {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) (s : Seq α) (s' : Seq β) (n : ) :
(zipWith f s s').get? n = Option.map₂ f (s.get? n) (s'.get? n)
@[simp]
theorem Stream'.Seq.get?_zip {α : Type u} {β : Type v} (s : Seq α) (t : Seq β) (n : ) :
(s.zip t).get? n = Option.map₂ Prod.mk (s.get? n) (t.get? n)
@[simp]
@[simp]
theorem Stream'.Seq.get?_enum {α : Type u} (s : Seq α) (n : ) :
@[simp]
theorem Stream'.Seq.zipWith_nil_left {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Seq β} :
@[simp]
theorem Stream'.Seq.zipWith_nil_right {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {s : Seq α} :
@[simp]
theorem Stream'.Seq.zipWith_cons_cons {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {x : α} {s : Seq α} {x' : β} {s' : Seq β} :
zipWith f (cons x s) (cons x' s') = cons (f x x') (zipWith f s s')
@[simp]
theorem Stream'.Seq.zip_nil_left {α : Type u} {s : Seq α} :
@[simp]
theorem Stream'.Seq.zip_nil_right {α : Type u} {s : Seq α} :
@[simp]
theorem Stream'.Seq.zip_cons_cons {α : Type u} {s s' : Seq α} {x x' : α} :
(cons x s).zip (cons x' s') = cons (x, x') (s.zip s')
@[simp]
@[simp]
theorem Stream'.Seq.enum_cons {α : Type u} (s : Seq α) (x : α) :
theorem Stream'.Seq.zipWith_map {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f₁ : αα') (f₂ : ββ') (g : α'β'γ) :
zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun (a : α) (b : β) => g (f₁ a) (f₂ b)) s₁ s₂
theorem Stream'.Seq.zipWith_map_left {α : Type u} {β : Type v} {γ : Type w} {α' : Type u'} (s₁ : Seq α) (s₂ : Seq β) (f : αα') (g : α'βγ) :
zipWith g (map f s₁) s₂ = zipWith (fun (a : α) (b : β) => g (f a) b) s₁ s₂
theorem Stream'.Seq.zipWith_map_right {α : Type u} {β : Type v} {γ : Type w} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f : ββ') (g : αβ'γ) :
zipWith g s₁ (map f s₂) = zipWith (fun (a : α) (b : β) => g a (f b)) s₁ s₂
theorem Stream'.Seq.zip_map {α : Type u} {β : Type v} {α' : Type u'} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f₁ : αα') (f₂ : ββ') :
(map f₁ s₁).zip (map f₂ s₂) = map (Prod.map f₁ f₂) (s₁.zip s₂)
theorem Stream'.Seq.zip_map_left {α : Type u} {β : Type v} {α' : Type u'} (s₁ : Seq α) (s₂ : Seq β) (f : αα') :
(map f s₁).zip s₂ = map (Prod.map f id) (s₁.zip s₂)
theorem Stream'.Seq.zip_map_right {α : Type u} {β : Type v} {β' : Type v'} (s₁ : Seq α) (s₂ : Seq β) (f : ββ') :
s₁.zip (map f s₂) = map (Prod.map id f) (s₁.zip s₂)
@[simp]
theorem Stream'.Seq.fold_nil {α : Type u} {β : Type v} (init : β) (f : βαβ) :
nil.fold init f = cons init nil
@[simp]
theorem Stream'.Seq.fold_cons {α : Type u} {β : Type v} (init : β) (f : βαβ) (x : α) (s : Seq α) :
(cons x s).fold init f = cons init (s.fold (f init x) f)
@[simp]
theorem Stream'.Seq.fold_head {α : Type u} {β : Type v} (init : β) (f : βαβ) (s : Seq α) :
(s.fold init f).head = some init
def Stream'.Seq1.toSeq {α : Type u} :
Seq1 αSeq α

Convert a Seq1 to a sequence.

Equations
instance Stream'.Seq1.coeSeq {α : Type u} :
Coe (Seq1 α) (Seq α)
Equations
def Stream'.Seq1.map {α : Type u} {β : Type v} (f : αβ) :
Seq1 αSeq1 β

Map a function on a Seq1

Equations
theorem Stream'.Seq1.map_pair {α : Type u} {β : Type v} {f : αβ} {a : α} {s : Seq α} :
map f (a, s) = (f a, Seq.map f s)
theorem Stream'.Seq1.map_id {α : Type u} (s : Seq1 α) :
map id s = s
def Stream'.Seq1.join {α : Type u} :
Seq1 (Seq1 α)Seq1 α

Flatten a nonempty sequence of nonempty sequences

Equations
@[simp]
theorem Stream'.Seq1.join_nil {α : Type u} (a : α) (S : Seq (Seq1 α)) :
@[simp]
theorem Stream'.Seq1.join_cons {α : Type u} (a b : α) (s : Seq α) (S : Seq (Seq1 α)) :
def Stream'.Seq1.ret {α : Type u} (a : α) :
Seq1 α

The return operator for the Seq1 monad, which produces a singleton sequence.

Equations
def Stream'.Seq1.bind {α : Type u} {β : Type v} (s : Seq1 α) (f : αSeq1 β) :
Seq1 β

The bind operator for the Seq1 monad, which maps f on each element of s and appends the results together. (Not all of s may be evaluated, because the first few elements of s may already produce an infinite result.)

Equations
@[simp]
theorem Stream'.Seq1.join_map_ret {α : Type u} (s : Seq α) :
@[simp]
theorem Stream'.Seq1.bind_ret {α : Type u} {β : Type v} (f : αβ) (s : Seq1 α) :
s.bind (ret f) = map f s
@[simp]
theorem Stream'.Seq1.ret_bind {α : Type u} {β : Type v} (a : α) (f : αSeq1 β) :
(ret a).bind f = f a
@[simp]
theorem Stream'.Seq1.map_join' {α : Type u} {β : Type v} (f : αβ) (S : Seq (Seq1 α)) :
@[simp]
theorem Stream'.Seq1.map_join {α : Type u} {β : Type v} (f : αβ) (S : Seq1 (Seq1 α)) :
map f S.join = (map (map f) S).join
@[simp]
theorem Stream'.Seq1.join_join {α : Type u} (SS : Seq (Seq1 (Seq1 α))) :
@[simp]
theorem Stream'.Seq1.bind_assoc {α : Type u} {β : Type v} {γ : Type w} (s : Seq1 α) (f : αSeq1 β) (g : βSeq1 γ) :
(s.bind f).bind g = s.bind fun (x : α) => (f x).bind g
Equations
  • One or more equations did not get rendered due to their size.