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 α] :
    Equations
    • Lean.SSet.empty = Lean.SMap.empty
    Instances For
      @[reducible, inline]
      abbrev Lean.SSet.insert {α : Type u} [BEq α] [Hashable α] (s : Lean.SSet α) (a : α) :
      Equations
      Instances For
        @[reducible, inline]
        abbrev Lean.SSet.contains {α : Type u} [BEq α] [Hashable α] (s : Lean.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 : Lean.SSet α) (f : αm PUnit) :
          Equations
          Instances For
            @[reducible, inline]
            abbrev Lean.SSet.switch {α : Type u} [BEq α] [Hashable α] (s : Lean.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 : Lean.SSet α) :
              σ
              Equations
              Instances For
                def Lean.SSet.toList {α : Type u} [BEq α] [Hashable α] (m : Lean.SSet α) :
                List α
                Equations
                Instances For
                  def List.toSSet {α : Type u_1} [BEq α] [Hashable α] (es : List α) :
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    instance instReprSSet {α : Type u_1} :
                    {x : BEq α} → {x_1 : Hashable α} → [inst : Repr α] → Repr (Lean.SSet α)
                    Equations