Documentation

Batteries.Lean.PersistentHashSet

instance Lean.PersistentHashSet.instForIn_batteries {α : Type u_1} [BEq α] [Hashable α] {m : Type u_2 → Type u_3} :
Equations
  • One or more equations did not get rendered due to their size.
@[specialize #[]]
def Lean.PersistentHashSet.anyM {α : Type u_1} [BEq α] [Hashable α] {m : TypeType u_2} [Monad m] (s : Lean.PersistentHashSet α) (f : αm Bool) :

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.PersistentHashSet.any {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PersistentHashSet α) (f : αBool) :

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

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

      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.PersistentHashSet.all {α : Type u_1} [BEq α] [Hashable α] (s : Lean.PersistentHashSet α) (f : αBool) :

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

        Equations
        • s.all f = (s.allM f).run
        Instances For
          Equations
          • Lean.PersistentHashSet.instBEq_batteries = { beq := fun (s t : Lean.PersistentHashSet α) => (s.all fun (x : α) => t.contains x) && t.all fun (x : α) => s.contains x }
          def Lean.PersistentHashSet.insertMany {α : Type u_1} [BEq α] [Hashable α] {ρ : Type u_2} [ForIn Id ρ α] (s : Lean.PersistentHashSet α) (as : ρ) :

          Insert all elements from a collection into a PersistentHashSet.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[inline]

            Obtain a PersistentHashSet from an array.

            Equations
            Instances For
              @[inline]

              Obtain a PersistentHashSet from a list.

              Equations
              Instances For
                @[inline]

                Merge two PersistentHashSets.

                Equations
                • s.merge t = s.insertMany t
                Instances For