Documentation

Aesop.Util.UnorderedArraySet

structure Aesop.UnorderedArraySet (α : Type u_1) [BEq α] :
Type u_1
Instances For
    Instances For
      @[implicit_reducible]
      instance Aesop.instInhabitedUnorderedArraySet {a✝ : Type u_1} {a✝¹ : BEq a✝} :

      O(1)

      Instances For

        O(1)

        Instances For

          O(n)

          Instances For

            Precondition: xs contains no duplicates.

            Instances For

              Precondition: xs is sorted.

              Instances For
                def Aesop.UnorderedArraySet.ofArray {α : Type u_1} [BEq α] [ord : Ord α] (xs : Array α) :

                O(n*log(n))

                Instances For

                  O(n^2)

                  Instances For
                    Instances For
                      Instances For

                        O(n)

                        Instances For
                          def Aesop.UnorderedArraySet.filterM {α : Type} [BEq α] {m : TypeType u_1} [Monad m] (p : αm Bool) (s : UnorderedArraySet α) :

                          O(n)

                          Instances For
                            def Aesop.UnorderedArraySet.filter {α : Type u_1} [BEq α] (p : αBool) (s : UnorderedArraySet α) :

                            O(n)

                            Instances For

                              O(n*m)

                              Instances For
                                @[implicit_reducible]
                                def Aesop.UnorderedArraySet.contains {α : Type u_1} [BEq α] (x : α) (s : UnorderedArraySet α) :

                                O(n)

                                Instances For
                                  def Aesop.UnorderedArraySet.foldM {α : Type u_1} [BEq α] {m : Type u_2 → Type u_3} {σ : Type u_2} [Monad m] (f : σαm σ) (init : σ) (s : UnorderedArraySet α) :
                                  m σ

                                  O(n)

                                  Instances For
                                    @[implicit_reducible]
                                    instance Aesop.UnorderedArraySet.instForInOfMonad {α : Type u_1} [BEq α] {m : Type u_2 → Type u_3} [Monad m] :
                                    def Aesop.UnorderedArraySet.fold {α : Type u_1} [BEq α] {σ : Type u_2} (f : σασ) (init : σ) (s : UnorderedArraySet α) :
                                    σ

                                    O(n)

                                    Instances For
                                      Instances For

                                        O(1)

                                        Instances For

                                          O(1)

                                          Instances For
                                            def Aesop.UnorderedArraySet.anyM {α : Type u_1} [BEq α] {m : TypeType u_2} [Monad m] (p : αm Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

                                            O(n)

                                            Instances For
                                              def Aesop.UnorderedArraySet.any {α : Type u_1} [BEq α] (p : αBool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

                                              O(n)

                                              Instances For
                                                def Aesop.UnorderedArraySet.allM {α : Type u_1} [BEq α] {m : TypeType u_2} [Monad m] (p : αm Bool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

                                                O(n)

                                                Instances For
                                                  def Aesop.UnorderedArraySet.all {α : Type u_1} [BEq α] (p : αBool) (s : UnorderedArraySet α) (start : Nat := 0) (stop : Nat := s.size) :

                                                  O(n)

                                                  Instances For
                                                    @[implicit_reducible]
                                                    @[implicit_reducible]