Documentation

Lake.Toml.Data.Dict

Red-Black Dictionary #

Defines an insertion-ordered key-value mapping backed by an red-black tree. Implemented via a key-index RBMap into an Array of key-value pairs.

structure Lake.Toml.RBDict (α : Type u) (β : Type v) (cmp : ααOrdering) :
Type (max u v)
Instances For
    instance Lake.Toml.instInhabitedRBDict :
    {a : Type u_1} → {a_1 : Type u_2} → {a_2 : aaOrdering} → Inhabited (Lake.Toml.RBDict a a_1 a_2)
    Equations
    • Lake.Toml.instInhabitedRBDict = { default := { items := default, indices := default } }
    @[reducible, inline]
    abbrev Lake.Toml.NameDict (α : Type u) :
    Type (max 0 u)
    Equations
    Instances For
      def Lake.Toml.RBDict.empty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
      Equations
      • Lake.Toml.RBDict.empty = { items := #[], indices := }
      Instances For
        instance Lake.Toml.RBDict.instEmptyCollection {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
        Equations
        • Lake.Toml.RBDict.instEmptyCollection = { emptyCollection := Lake.Toml.RBDict.empty }
        def Lake.Toml.RBDict.mkEmpty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (capacity : Nat) :
        Equations
        Instances For
          def Lake.Toml.RBDict.ofArray {α : Type (max u_1 u_2)} {β : Type u_2} {cmp : ααOrdering} (items : Array (α × β)) :
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def Lake.Toml.RBDict.beq {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} [BEq (α × β)] (self : Lake.Toml.RBDict α β cmp) (other : Lake.Toml.RBDict α β cmp) :
            Equations
            • self.beq other = (self.items == other.items)
            Instances For
              instance Lake.Toml.RBDict.instBEqOfProd {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} [BEq (α × β)] :
              BEq (Lake.Toml.RBDict α β cmp)
              Equations
              • Lake.Toml.RBDict.instBEqOfProd = { beq := Lake.Toml.RBDict.beq }
              @[reducible, inline]
              abbrev Lake.Toml.RBDict.size {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Lake.Toml.RBDict α β cmp) :
              Equations
              • t.size = t.items.size
              Instances For
                @[reducible, inline]
                abbrev Lake.Toml.RBDict.isEmpty {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Lake.Toml.RBDict α β cmp) :
                Equations
                • t.isEmpty = t.items.isEmpty
                Instances For
                  def Lake.Toml.RBDict.keys {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Lake.Toml.RBDict α β cmp) :
                  Equations
                  Instances For
                    def Lake.Toml.RBDict.values {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Lake.Toml.RBDict α β cmp) :
                    Equations
                    Instances For
                      def Lake.Toml.RBDict.contains {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (t : Lake.Toml.RBDict α β cmp) :
                      Equations
                      Instances For
                        def Lake.Toml.RBDict.findIdx? {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (t : Lake.Toml.RBDict α β cmp) :
                        Option (Fin t.size)
                        Equations
                        Instances For
                          def Lake.Toml.RBDict.findEntry? {α : Type} {β : Type} {cmp : ααOrdering} (k : α) (t : Lake.Toml.RBDict α β cmp) :
                          Option (α × β)
                          Equations
                          Instances For
                            @[inline]
                            def Lake.Toml.RBDict.find? {α : Type} {β : Type} {cmp : ααOrdering} (k : α) (t : Lake.Toml.RBDict α β cmp) :
                            Equations
                            Instances For
                              def Lake.Toml.RBDict.push {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (v : β) (t : Lake.Toml.RBDict α β cmp) :
                              Equations
                              Instances For
                                @[specialize #[]]
                                def Lake.Toml.RBDict.alter {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (f : Option ββ) (t : Lake.Toml.RBDict α β cmp) :
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For
                                  def Lake.Toml.RBDict.insert {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (v : β) (t : Lake.Toml.RBDict α β cmp) :
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    @[macro_inline]
                                    def Lake.Toml.RBDict.insertIf {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (p : Bool) (k : α) (v : β) (t : Lake.Toml.RBDict α β cmp) :

                                    Inserts the value into the dictionary if p is true.

                                    Equations
                                    Instances For
                                      @[macro_inline]
                                      def Lake.Toml.RBDict.insertUnless {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (p : Bool) (k : α) (v : β) (t : Lake.Toml.RBDict α β cmp) :

                                      Inserts the value into the dictionary if p is false.

                                      Equations
                                      Instances For
                                        @[macro_inline]
                                        def Lake.Toml.RBDict.insertSome {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (k : α) (v? : Option β) (t : Lake.Toml.RBDict α β cmp) :

                                        Insert the value into the dictionary if it is not none.

                                        Equations
                                        Instances For
                                          def Lake.Toml.RBDict.appendArray {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.Toml.RBDict α β cmp) (other : Array (α × β)) :
                                          Equations
                                          Instances For
                                            instance Lake.Toml.RBDict.instHAppendArrayProd {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                                            HAppend (Lake.Toml.RBDict α β cmp) (Array (α × β)) (Lake.Toml.RBDict α β cmp)
                                            Equations
                                            • Lake.Toml.RBDict.instHAppendArrayProd = { hAppend := Lake.Toml.RBDict.appendArray }
                                            @[inline]
                                            def Lake.Toml.RBDict.append {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (self : Lake.Toml.RBDict α β cmp) (other : Lake.Toml.RBDict α β cmp) :
                                            Equations
                                            • self.append other = self.appendArray other.items
                                            Instances For
                                              instance Lake.Toml.RBDict.instAppend {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
                                              Equations
                                              • Lake.Toml.RBDict.instAppend = { append := Lake.Toml.RBDict.append }
                                              @[inline]
                                              def Lake.Toml.RBDict.map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : ααOrdering} (f : αβγ) (t : Lake.Toml.RBDict α β cmp) :
                                              Equations
                                              Instances For
                                                @[inline]
                                                def Lake.Toml.RBDict.filter {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (p : αβBool) (t : Lake.Toml.RBDict α β cmp) :
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  @[inline]
                                                  def Lake.Toml.RBDict.filterMap {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : ααOrdering} (f : αβOption γ) (t : Lake.Toml.RBDict α β cmp) :
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For