Documentation

Lean.Data.PersistentHashSet

source
structure Lean.PersistentHashSet (α : Type u) [BEq α] [Hashable α] :
Type u
Instances For
    source
    @[reducible, inline]
    abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] :
    Type u
    Instances For
      source
      @[inline]
      def Lean.PersistentHashSet.empty {α : Type u_1} [BEq α] [Hashable α] :
      PersistentHashSet α
      Instances For
        source
        @[instance_reducible]
        instance Lean.PersistentHashSet.instInhabited {α : Type u_1} [BEq α] [Hashable α] :
        Inhabited (PersistentHashSet α)
        source
        @[instance_reducible]
        instance Lean.PersistentHashSet.instEmptyCollection {α : Type u_1} [BEq α] [Hashable α] :
        EmptyCollection (PersistentHashSet α)
        source
        @[inline]
        def Lean.PersistentHashSet.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
        Bool
        Instances For
          source
          @[inline]
          def Lean.PersistentHashSet.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
          PersistentHashSet α
          Instances For
            source
            @[inline]
            def Lean.PersistentHashSet.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
            PersistentHashSet α
            Instances For
              source
              @[inline]
              def Lean.PersistentHashSet.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
              Option α
              Instances For
                source
                @[inline]
                def Lean.PersistentHashSet.findD {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a a₀ : α) :
                α
                Instances For
                  source
                  @[inline]
                  def Lean.PersistentHashSet.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
                  Bool
                  Instances For
                    source
                    @[inline]
                    def Lean.PersistentHashSet.foldM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Type v → Type w} [Monad m] (f : β → α → m β) (init : β) (s : PersistentHashSet α) :
                    m β
                    Instances For
                      source
                      @[inline]
                      def Lean.PersistentHashSet.fold {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (f : β → α → β) (init : β) (s : PersistentHashSet α) :
                      β
                      Instances For
                        source
                        def Lean.PersistentHashSet.toList {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
                        List α
                        Instances For
                          source
                          def Lean.PersistentHashSet.forIn {α : Type u_1} {m : Type u_2 → Type u_3} {σ : Type u_2} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] (s : PersistentHashSet α) (init : σ) (f : α → σ → m (ForInStep σ)) :
                          m σ
                          Instances For
                            source
                            @[instance_reducible]
                            instance Lean.PersistentHashSet.instForInOfMonad {α : Type u_1} {m : Type u_2 → Type u_3} {x✝ : BEq α} {x✝¹ : Hashable α} [Monad m] :
                            ForIn m (PersistentHashSet α) α