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.instCoeOrdHashSetHashSet = { coe := Lake.OrdHashSet.toHashSet }
    Equations
    • Lake.OrdHashSet.empty = { toHashSet := Lean.HashSet.empty, toArray := #[] }
    Instances For
      Equations
      • Lake.OrdHashSet.instEmptyCollectionOrdHashSet = { 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
        Instances For
          def Lake.OrdHashSet.appendArray {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (arr : Array α) :
          Equations
          Instances For
            Equations
            • Lake.OrdHashSet.instHAppendOrdHashSetArray = { hAppend := Lake.OrdHashSet.appendArray }
            def Lake.OrdHashSet.append {α : Type u_1} [Hashable α] [BEq α] (self : Lake.OrdHashSet α) (other : Lake.OrdHashSet α) :
            Equations
            Instances For
              Equations
              • Lake.OrdHashSet.instAppendOrdHashSet = { append := Lake.OrdHashSet.append }
              @[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
                            Instances For
                              instance Lake.OrdHashSet.instForInOrdHashSet {α : Type u_1} [Hashable α] [BEq α] {m : Type u_2 → Type u_3} :
                              Equations
                              • Lake.OrdHashSet.instForInOrdHashSet = { forIn := fun {β} [Monad m] => Lake.OrdHashSet.forIn }