Documentation

Std.Data.DTreeMap.Internal.Cell

The Cell type #

structure Std.DTreeMap.Internal.Cell (α : Type u) [Ord α] (β : αType v) (k : αOrdering) :
Type (max u v)

Type for representing the place in a tree map where a mapping for k could live. Internal implementation detail of the tree map.

Instances For
    def Std.DTreeMap.Internal.Cell.ofEq {α : Type u} {β : αType v} [Ord α] {k : αOrdering} (k' : α) (v' : β k') (hcmp : ∀ [OrientedOrd α], k k' = Ordering.eq) :
    Cell α β k

    Create a cell with a matching key. Internal implementation detail of the tree map

    Equations
      Instances For
        def Std.DTreeMap.Internal.Cell.of {α : Type u} {β : αType v} [Ord α] (k : α) (v : β k) :
        Cell α β (compare k)

        Create a cell with a matching key. Internal implementation detail of the tree map

        Equations
          Instances For
            @[simp]
            theorem Std.DTreeMap.Internal.Cell.ofEq_inner {α : Type u} {β : αType v} [Ord α] {k : αOrdering} {k' : α} {v' : β k'} {h : ∀ [OrientedOrd α], k k' = Ordering.eq} :
            (ofEq k' v' h).inner = some k', v'
            @[simp]
            theorem Std.DTreeMap.Internal.Cell.of_inner {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} :
            (of k v).inner = some k, v
            def Std.DTreeMap.Internal.Cell.empty {α : Type u} {β : αType v} [Ord α] {k : αOrdering} :
            Cell α β k

            Create an empty cell. Internal implementation detail of the tree map

            Equations
              Instances For
                def Std.DTreeMap.Internal.Cell.ofOption {α : Type u} {β : αType v} [Ord α] (k : α) (v? : Option (β k)) :
                Cell α β (compare k)

                Internal implementation detail of the tree map

                Equations
                  Instances For
                    @[simp]
                    theorem Std.DTreeMap.Internal.Cell.empty_inner {α : Type u} {β : αType v} [Ord α] {k : αOrdering} :
                    def Std.DTreeMap.Internal.Cell.contains {α : Type u} {β : αType v} [Ord α] {k : αOrdering} (c : Cell α β k) :

                    Internal implementation detail of the tree map

                    Equations
                      Instances For
                        @[simp]
                        theorem Std.DTreeMap.Internal.Cell.contains_of {α : Type u} {β : αType v} [Ord α] {k : α} {v : β k} :
                        @[simp]
                        theorem Std.DTreeMap.Internal.Cell.contains_ofEq {α : Type u} {β : αType v} [Ord α] {k : αOrdering} {k' : α} {v' : β k'} {h : ∀ [OrientedOrd α], k k' = Ordering.eq} :
                        (ofEq k' v' h).contains = true
                        @[simp]
                        theorem Std.DTreeMap.Internal.Cell.contains_empty {α : Type u} {β : αType v} [Ord α] {k : αOrdering} :
                        def Std.DTreeMap.Internal.Cell.get? {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} (c : Cell α β (compare k)) :
                        Option (β k)

                        Internal implementation detail of the tree map

                        Equations
                          Instances For
                            @[simp]
                            theorem Std.DTreeMap.Internal.Cell.get?_empty {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} :
                            def Std.DTreeMap.Internal.Cell.getKey? {α : Type u} {β : αType v} [Ord α] {k : α} (c : Cell α β (compare k)) :

                            Internal implementation detail of the tree map

                            Equations
                              Instances For
                                @[simp]
                                theorem Std.DTreeMap.Internal.Cell.getKey?_empty {α : Type u} {β : αType v} [Ord α] {k : α} :
                                def Std.DTreeMap.Internal.Cell.alter {α : Type u} {β : αType v} [Ord α] [OrientedOrd α] [LawfulEqOrd α] {k : α} (f : Option (β k)Option (β k)) (c : Cell α β (compare k)) :
                                Cell α β (compare k)

                                Internal implementation detail of the tree map

                                Equations
                                  Instances For
                                    theorem Std.DTreeMap.Internal.Cell.ext {α : Type u} {β : αType v} [Ord α] {k : αOrdering} {c c' : Cell α β k} :
                                    c.inner = c'.innerc = c'
                                    def Std.DTreeMap.Internal.Cell.Const.get? {α : Type u} {β : Type v} [Ord α] {k : α} (c : Cell α (fun (x : α) => β) (compare k)) :

                                    Internal implementation detail of the tree map

                                    Equations
                                      Instances For
                                        @[simp]
                                        theorem Std.DTreeMap.Internal.Cell.Const.get?_empty {α : Type u} {β : Type v} [Ord α] {k : α} :
                                        def Std.DTreeMap.Internal.Cell.Const.alter {α : Type u} {β : Type v} [Ord α] [OrientedOrd α] {k : α} (f : Option βOption β) (c : Cell α (fun (x : α) => β) (compare k)) :
                                        Cell α (fun (x : α) => β) (compare k)

                                        Internal implementation detail of the tree map

                                        Equations
                                          Instances For
                                            def Std.DTreeMap.Internal.List.findCell {α : Type u} {β : αType v} [Ord α] (l : List ((a : α) × β a)) (k : αOrdering) :
                                            Cell α β k

                                            Internal implementation detail of the tree map

                                            Equations
                                              Instances For
                                                theorem Std.DTreeMap.Internal.List.findCell_inner {α : Type u} {β : αType v} [Ord α] (l : List ((a : α) × β a)) (k : αOrdering) :
                                                (findCell l k).inner = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l
                                                @[simp]
                                                theorem Std.DTreeMap.Internal.List.findCell_nil {α : Type u} {β : αType v} [Ord α] (k : αOrdering) :