Documentation

Batteries.Lean.PersistentHashSet

instance Lean.PersistentHashSet.instForIn_batteries {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} :
Equations
    @[specialize #[]]
    def Lean.PersistentHashSet.anyM {α : Type u_1} [BEq α] [Hashable α] {m : TypeType u_2} [Monad m] (s : PersistentHashSet α) (f : αm Bool) :

    Returns true if f returns true for any element of the set.

    Equations
      Instances For
        @[inline]
        def Lean.PersistentHashSet.any {α : Type u_1} [BEq α] [Hashable α] (s : PersistentHashSet α) (f : αBool) :

        Returns true if f returns true for any element of the set.

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

            Returns true if f returns true for all elements of the set.

            Equations
              Instances For
                @[inline]
                def Lean.PersistentHashSet.all {α : Type u_1} [BEq α] [Hashable α] (s : PersistentHashSet α) (f : αBool) :

                Returns true if f returns true for all elements of the set.

                Equations
                  Instances For
                    def Lean.PersistentHashSet.insertMany {α : Type u_1} [BEq α] [Hashable α] {ρ : Type u_2} [ForIn Id ρ α] (s : PersistentHashSet α) (as : ρ) :

                    Insert all elements from a collection into a PersistentHashSet.

                    Equations
                      Instances For
                        @[inline]

                        Obtain a PersistentHashSet from an array.

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

                            Obtain a PersistentHashSet from a list.

                            Equations
                              Instances For
                                @[inline]

                                Merge two PersistentHashSets.

                                Equations
                                  Instances For