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 α.

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

    Prepend an element to a stream.

    Equations
    Instances For
      def Stream'.get {α : Type u} (s : Stream' α) (n : ) :
      α

      Get the n-th element of a stream.

      Equations
      • s.get n = s n
      Instances For
        @[reducible, inline]
        abbrev Stream'.head {α : Type u} (s : Stream' α) :
        α

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

        Equations
        • s.head = s.get 0
        Instances For
          def Stream'.tail {α : Type u} (s : Stream' α) :

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

          Equations
          • s.tail i = s.get (i + 1)
          Instances For
            def Stream'.drop {α : Type u} (n : ) (s : Stream' α) :

            Drop first n elements of a stream.

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

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

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

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

                Equations
                Instances For
                  instance Stream'.instMembership {α : Type u} :

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

                  Equations
                  • Stream'.instMembership = { mem := fun (s : Stream' α) (a : α) => Stream'.Any (fun (b : α) => a = b) s }
                  def Stream'.map {α : Type u} {β : Type v} (f : αβ) (s : Stream' α) :

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

                  Equations
                  Instances For
                    def Stream'.zip {α : Type u} {β : Type v} {δ : Type w} (f : αβδ) (s₁ : Stream' α) (s₂ : Stream' β) :

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

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

                      Enumerate a stream by tagging each element with its index.

                      Equations
                      • s.enum n = (n, s.get n)
                      Instances For
                        def Stream'.const {α : Type u} (a : α) :

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

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

                          Iterates of a function as a stream.

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

                                  Use a state monad to generate a stream through corecursion

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

                                      Interleave two streams.

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

                                        Elements of a stream with even indices.

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

                                          Elements of a stream with odd indices.

                                          Equations
                                          • s.odd = s.tail.even
                                          Instances For
                                            def Stream'.appendStream' {α : Type u} :
                                            List αStream' αStream' α

                                            Append a stream to a list.

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

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

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

                                                An auxiliary definition for Stream'.cycle corecursive def

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

                                                  An auxiliary definition for Stream'.cycle corecursive def

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

                                                    Interpret a nonempty list as a cyclic stream.

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

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

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

                                                        An auxiliary definition for Stream'.inits.

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

                                                          Nonempty initial segments of a stream.

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

                                                            A constant stream, same as Stream'.const.

                                                            Equations
                                                            Instances For
                                                              def Stream'.apply {α : Type u} {β : Type v} (f : Stream' (αβ)) (s : Stream' α) :

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

                                                              Equations
                                                              • (f s) n = f.get n (s.get n)
                                                              Instances For

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

                                                                Equations
                                                                Instances For