Documentation

Std.Lean.HashSet

Equations
  • Lean.HashSet.instSingletonHashSet = { singleton := fun (x : α) => Lean.HashSet.insert Lean.HashSet.empty x }
instance Lean.HashSet.instInsertHashSet {α : Type u_1} [BEq α] [Hashable α] :
Equations
@[specialize #[]]
def Lean.HashSet.anyM {α : Type u_1} [BEq α] [Hashable α] {m : TypeType} [Monad m] (s : Lean.HashSet α) (f : αm Bool) :

O(n). Returns true if f returns true for any element of the set.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[inline]
    def Lean.HashSet.any {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (f : αBool) :

    O(n). Returns true if f returns true for any element of the set.

    Equations
    Instances For
      @[specialize #[]]
      def Lean.HashSet.allM {α : Type u_1} [BEq α] [Hashable α] {m : TypeType} [Monad m] (s : Lean.HashSet α) (f : αm Bool) :

      O(n). Returns true if f returns true for all elements of the set.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[inline]
        def Lean.HashSet.all {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (f : αBool) :

        O(n). Returns true if f returns true for all elements of the set.

        Equations
        Instances For
          instance Lean.HashSet.instBEqHashSet {α : Type u_1} [BEq α] [Hashable α] :
          Equations
          • One or more equations did not get rendered due to their size.
          @[inline]
          def Lean.HashSet.insert' {α : Type u_1} [BEq α] [Hashable α] (s : Lean.HashSet α) (a : α) :

          O(1) amortized. Similar to insert, but also returns a Boolean flag indicating whether an existing entry has been replaced with a => b.

          Equations
          Instances For
            @[inline]
            def Lean.HashSet.ofArray {α : Type u_1} [BEq α] [Hashable α] (as : Array α) :

            O(n). Obtain a HashSet from an array.

            Equations
            Instances For
              @[inline]
              def Lean.HashSet.ofList {α : Type u_1} [BEq α] [Hashable α] (as : List α) :

              O(n). Obtain a HashSet from a list.

              Equations
              Instances For
                @[inline]
                def Lean.HashSet.merge {α : Type u} [BEq α] [Hashable α] (s : Lean.HashSet α) (t : Lean.HashSet α) :

                O(|t|) amortized. Merge two HashSets.

                Equations
                Instances For