Documentation

Lean.Data.PersistentHashSet

structure Lean.PersistentHashSet (α : Type u) [BEq α] [Hashable α] :
Instances For
    @[reducible, inline]
    abbrev Lean.PHashSet (α : Type u) [BEq α] [Hashable α] :
    Equations
      Instances For
        @[inline]
        Equations
          Instances For
            @[inline]
            def Lean.PersistentHashSet.isEmpty {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
            Equations
              Instances For
                @[inline]
                def Lean.PersistentHashSet.insert {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
                Equations
                  Instances For
                    @[inline]
                    def Lean.PersistentHashSet.erase {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
                    Equations
                      Instances For
                        @[inline]
                        def Lean.PersistentHashSet.find? {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
                        Equations
                          Instances For
                            @[inline]
                            def Lean.PersistentHashSet.contains {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) (a : α) :
                            Equations
                              Instances For
                                @[inline]
                                def Lean.PersistentHashSet.foldM {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} {m : Type v → Type v} [Monad m] (f : βαm β) (init : β) (s : PersistentHashSet α) :
                                m β
                                Equations
                                  Instances For
                                    @[inline]
                                    def Lean.PersistentHashSet.fold {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} {β : Type v} (f : βαβ) (init : β) (s : PersistentHashSet α) :
                                    β
                                    Equations
                                      Instances For
                                        def Lean.PersistentHashSet.toList {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} (s : PersistentHashSet α) :
                                        List α
                                        Equations
                                          Instances For
                                            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 σ
                                            Equations
                                              Instances For
                                                instance Lean.PersistentHashSet.instForIn {α : Type u_1} {m : Type u_2 → Type u_3} {x✝ : BEq α} {x✝¹ : Hashable α} :
                                                Equations