Documentation

Lean.Data.SSet

def Lean.SSet (α : Type u) [BEq α] [Hashable α] :

Staged set. It is just a simple wrapper on top of Staged maps.

Equations
    Instances For
      instance Lean.SSet.instInhabited {α : Type u} [BEq α] [Hashable α] :
      Equations
        @[reducible, inline]
        abbrev Lean.SSet.empty {α : Type u} [BEq α] [Hashable α] :
        SSet α
        Equations
          Instances For
            @[reducible, inline]
            abbrev Lean.SSet.insert {α : Type u} [BEq α] [Hashable α] (s : SSet α) (a : α) :
            SSet α
            Equations
              Instances For
                @[reducible, inline]
                abbrev Lean.SSet.contains {α : Type u} [BEq α] [Hashable α] (s : SSet α) (a : α) :
                Equations
                  Instances For
                    @[reducible, inline]
                    abbrev Lean.SSet.forM {α : Type u} [BEq α] [Hashable α] {m : Type u_1 → Type u_1} [Monad m] (s : SSet α) (f : αm PUnit) :
                    Equations
                      Instances For
                        @[reducible, inline]
                        abbrev Lean.SSet.switch {α : Type u} [BEq α] [Hashable α] (s : SSet α) :
                        SSet α

                        Move from stage 1 into stage 2.

                        Equations
                          Instances For
                            @[reducible, inline]
                            abbrev Lean.SSet.fold {α : Type u} [BEq α] [Hashable α] {σ : Type u_1} (f : σασ) (init : σ) (s : SSet α) :
                            σ
                            Equations
                              Instances For
                                def Lean.SSet.toList {α : Type u} [BEq α] [Hashable α] (m : SSet α) :
                                List α
                                Equations
                                  Instances For
                                    def List.toSSet {α : Type u_1} [BEq α] [Hashable α] (es : List α) :
                                    Equations
                                      Instances For
                                        instance instReprSSet {α : Type u_1} {x✝ : BEq α} {x✝¹ : Hashable α} [Repr α] :
                                        Equations