Documentation

Mathlib.Data.Stream.Defs

Definition of Stream' and functions on streams #

A stream Stream' α is an infinite sequence of elements of α. One can also think about it as an infinite list. In this file we define Stream' and some functions that take and/or return streams. Note that we already have Stream to represent a similar object, hence the awkward naming.

def Stream' (α : Type u) :

A stream Stream' α is an infinite sequence of elements of α.

Instances For
    def Stream'.cons {α : Type u_1} (a : α) (s : Stream' α) :

    Prepend an element to a stream.

    Instances For
      def Stream'.nth {α : Type u_1} (s : Stream' α) (n : ) :
      α

      n-th element of a stream.

      Instances For
        @[inline, reducible]
        abbrev Stream'.head {α : Type u_1} (s : Stream' α) :
        α

        Head of a stream: Stream'.head s = Stream'.nth s 0.

        Instances For
          def Stream'.tail {α : Type u_1} (s : Stream' α) :

          Tail of a stream: Stream'.tail (h :: t) = t.

          Instances For
            def Stream'.drop {α : Type u_1} (n : ) (s : Stream' α) :

            Drop first n elements of a stream.

            Instances For
              def Stream'.All {α : Type u_1} (p : αProp) (s : Stream' α) :

              Proposition saying that all elements of a stream satisfy a predicate.

              Instances For
                def Stream'.Any {α : Type u_1} (p : αProp) (s : Stream' α) :

                Proposition saying that at least one element of a stream satisfies a predicate.

                Instances For

                  a ∈ s means that a = Stream'.nth n s for some n.

                  def Stream'.map {α : Type u_1} {β : Type u_2} (f : αβ) (s : Stream' α) :

                  Apply a function f to all elements of a stream s.

                  Instances For
                    def Stream'.zip {α : Type u_1} {β : Type u_2} {δ : Type u_3} (f : αβδ) (s₁ : Stream' α) (s₂ : Stream' β) :

                    Zip two streams using a binary operation: Stream'.nth n (Stream'.zip f s₁ s₂) = f (Stream'.nth s₁) (Stream'.nth s₂).

                    Instances For
                      def Stream'.enum {α : Type u_1} (s : Stream' α) :

                      Enumerate a stream by tagging each element with its index.

                      Instances For
                        def Stream'.const {α : Type u_1} (a : α) :

                        The constant stream: Stream'.nth n (Stream'.const a) = a.

                        Instances For
                          def Stream'.iterate {α : Type u_1} (f : αα) (a : α) :

                          Iterates of a function as a stream.

                          Equations
                          Instances For
                            def Stream'.corec {α : Type u_1} {β : Type u_2} (f : αβ) (g : αα) :
                            αStream' β
                            Instances For
                              def Stream'.corecOn {α : Type u_1} {β : Type u_2} (a : α) (f : αβ) (g : αα) :
                              Instances For
                                def Stream'.corec' {α : Type u_1} {β : Type u_2} (f : αβ × α) :
                                αStream' β
                                Instances For
                                  def Stream'.corecState {σ : Type u_1} {α : Type u_1} (cmd : StateM σ α) (s : σ) :

                                  Use a state monad to generate a stream through corecursion

                                  Instances For
                                    @[inline, reducible]
                                    abbrev Stream'.unfolds {α : Type u_1} {β : Type u_2} (g : αβ) (f : αα) (a : α) :
                                    Instances For
                                      def Stream'.interleave {α : Type u_1} (s₁ : Stream' α) (s₂ : Stream' α) :

                                      Interleave two streams.

                                      Instances For
                                        def Stream'.even {α : Type u_1} (s : Stream' α) :

                                        Elements of a stream with even indices.

                                        Instances For
                                          def Stream'.odd {α : Type u_1} (s : Stream' α) :

                                          Elements of a stream with odd indices.

                                          Instances For
                                            def Stream'.appendStream' {α : Type u_1} :
                                            List αStream' αStream' α

                                            Append a stream to a list.

                                            Equations
                                            Instances For
                                              def Stream'.take {α : Type u_1} :
                                              Stream' αList α

                                              take n s returns a list of the n first elements of stream s

                                              Equations
                                              Instances For
                                                def Stream'.cycleF {α : Type u_1} :
                                                α × List α × α × List αα

                                                An auxiliary definition for Stream'.cycle corecursive def

                                                Instances For
                                                  def Stream'.cycleG {α : Type u_1} :
                                                  α × List α × α × List αα × List α × α × List α

                                                  An auxiliary definition for Stream'.cycle corecursive def

                                                  Instances For
                                                    def Stream'.cycle {α : Type u_1} (l : List α) :
                                                    l []Stream' α

                                                    Interpret a nonempty list as a cyclic stream.

                                                    Instances For
                                                      def Stream'.tails {α : Type u_1} (s : Stream' α) :

                                                      Tails of a stream, starting with Stream'.tail s.

                                                      Instances For
                                                        def Stream'.initsCore {α : Type u_1} (l : List α) (s : Stream' α) :

                                                        An auxiliary definition for Stream'.inits.

                                                        Instances For
                                                          def Stream'.inits {α : Type u_1} (s : Stream' α) :

                                                          Nonempty initial segments of a stream.

                                                          Instances For
                                                            def Stream'.pure {α : Type u_1} (a : α) :

                                                            A constant stream, same as Stream'.const.

                                                            Instances For
                                                              def Stream'.apply {α : Type u_1} {β : Type u_2} (f : Stream' (αβ)) (s : Stream' α) :

                                                              Given a stream of functions and a stream of values, apply n-th function to n-th value.

                                                              Instances For

                                                                The stream of natural numbers: Stream'.nth n Stream'.nats = n.

                                                                Instances For