Documentation

Lake.Util.OrdHashSet

structure Lake.OrdHashSet (α : Type u_1) [Hashable α] [BEq α] :
Type u_1

A HashSet that preserves insertion order.

Instances For
    Equations
    • Lake.OrdHashSet.instCoeHashSet = { coe := Lake.OrdHashSet.toHashSet }
    Equations
    • Lake.OrdHashSet.empty = { toHashSet := Std.HashSet.empty, toArray := #[] }
    Instances For
      Equations
      • Lake.OrdHashSet.instEmptyCollection = { emptyCollection := Lake.OrdHashSet.empty }
      def Lake.OrdHashSet.mkEmpty {α : Type u_1} [Hashable α] [BEq α] (size : Nat) :
      Equations
      Instances For
        def Lake.OrdHashSet.insert {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (a : α) :
        Equations
        • self.insert a = if self.toHashSet.contains a = true then self else { toHashSet := self.toHashSet.insert a, toArray := self.toArray.push a }
        Instances For
          def Lake.OrdHashSet.appendArray {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (arr : Array α) :
          Equations
          Instances For
            Equations
            • Lake.OrdHashSet.instHAppendArray = { hAppend := Lake.OrdHashSet.appendArray }
            def Lake.OrdHashSet.append {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (other : Lake.OrdHashSet α) :
            Equations
            • self.append other = self.appendArray other.toArray
            Instances For
              Equations
              • Lake.OrdHashSet.instAppend = { append := Lake.OrdHashSet.append }
              def Lake.OrdHashSet.ofArray {α : Type u_1} [Hashable α] [BEq α] (arr : Array α) :
              Equations
              Instances For
                @[inline]
                def Lake.OrdHashSet.all {α : Type u_1} [Hashable α] [BEq α] (f : αBool) (self : Lake.OrdHashSet α) :
                Equations
                Instances For
                  @[inline]
                  def Lake.OrdHashSet.any {α : Type u_1} [Hashable α] [BEq α] (f : αBool) (self : Lake.OrdHashSet α) :
                  Equations
                  Instances For
                    @[inline]
                    def Lake.OrdHashSet.foldl {α : Type u_1} [Hashable α] [BEq α] {β : Type u_2} (f : βαβ) (init : β) (self : Lake.OrdHashSet α) :
                    β
                    Equations
                    Instances For
                      @[inline]
                      def Lake.OrdHashSet.foldlM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : βαm β) (init : β) (self : Lake.OrdHashSet α) :
                      m β
                      Equations
                      Instances For
                        @[inline]
                        def Lake.OrdHashSet.foldr {α : Type u_1} [Hashable α] [BEq α] {β : Type u_2} (f : αββ) (init : β) (self : Lake.OrdHashSet α) :
                        β
                        Equations
                        Instances For
                          @[inline]
                          def Lake.OrdHashSet.foldrM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (f : αβm β) (init : β) (self : Lake.OrdHashSet α) :
                          m β
                          Equations
                          Instances For
                            @[inline]
                            def Lake.OrdHashSet.forM {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} [Monad m] (f : αm PUnit) (self : Lake.OrdHashSet α) :
                            Equations
                            Instances For
                              @[inline]
                              def Lake.OrdHashSet.forIn {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} {β : Type u_2} [Monad m] (self : Lake.OrdHashSet α) (init : β) (f : αβm (ForInStep β)) :
                              m β
                              Equations
                              • self.forIn init f = self.toArray.forIn init f
                              Instances For
                                instance Lake.OrdHashSet.instForIn {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} :
                                Equations
                                • Lake.OrdHashSet.instForIn = { forIn := fun {β : Type ?u.32} [Monad m] => Lake.OrdHashSet.forIn }