Documentation

Aesop.Util.UnorderedArraySet

structure Aesop.UnorderedArraySet (α : Type u_1) [BEq α] :
Type u_1
Instances For
    Equations
    • Aesop.instInhabitedUnorderedArraySet = { default := { rep := default } }

    O(1)

    Equations
    • Aesop.UnorderedArraySet.empty = { rep := #[] }
    Instances For
      Equations
      • Aesop.UnorderedArraySet.instEmptyCollectionUnorderedArraySet = { emptyCollection := Aesop.UnorderedArraySet.empty }

      O(1)

      Equations
      Instances For

        O(n)

        Equations
        Instances For

          Precondition: xs contains no duplicates.

          Equations
          Instances For

            Precondition: xs is sorted.

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

              O(n*log(n))

              Equations
              Instances For

                O(n)

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

                  O(n)

                  Equations
                  Instances For

                    O(n)

                    Equations
                    Instances For
                      Equations
                      • Aesop.UnorderedArraySet.instAppendUnorderedArraySet = { append := Aesop.UnorderedArraySet.merge }

                      O(n)

                      Equations
                      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 : Aesop.UnorderedArraySet α) :
                        m σ

                        O(n)

                        Equations
                        Instances For
                          Equations
                          • Aesop.UnorderedArraySet.instForInUnorderedArraySet = { forIn := fun {β} [Monad m] s => Array.forIn s.rep }
                          def Aesop.UnorderedArraySet.fold {α : Type u_1} [BEq α] {σ : Type u_2} (f : σασ) (init : σ) (s : Aesop.UnorderedArraySet α) :
                          σ

                          O(n)

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

                              O(n)

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

                                O(n)

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

                                  O(n)

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

                                    O(n)

                                    Equations
                                    Instances For
                                      Equations
                                      • Aesop.UnorderedArraySet.instBEqUnorderedArraySet = { beq := fun s t => Array.equalSet s.rep t.rep }
                                      Equations
                                      • Aesop.UnorderedArraySet.instToStringUnorderedArraySet = { toString := fun s => toString s.rep }
                                      Equations
                                      • Aesop.UnorderedArraySet.instToFormatUnorderedArraySet = { format := fun s => Std.format s.rep }
                                      Equations
                                      • Aesop.UnorderedArraySet.instToMessageDataUnorderedArraySet = { toMessageData := fun s => Lean.toMessageData s.rep }