Documentation

Lake.Util.DRBMap

This module includes a dependently typed adaption of the Lean.RBMap defined in Lean.Data.RBMap module of the Lean core. Most of the code is copied directly from there with only minor edits.

Equations
  • Lake.inhabitedOfEmptyCollection = { default := }
@[specialize #[]]
def Lake.RBNode.dFind {α : Type u} {β : αType v} (cmp : ααOrdering) [h : Lake.EqOfCmpWrt α β cmp] :
Lean.RBNode α β(k : α) → Option (β k)
Equations
  • One or more equations did not get rendered due to their size.
  • Lake.RBNode.dFind cmp Lean.RBNode.leaf x = none
Instances For
    def Lake.DRBMap (α : Type u) (β : αType v) (cmp : ααOrdering) :
    Type (max u v)

    A Dependently typed RBMap.

    Equations
    Instances For
      instance Lake.instCoeDRBMapRBMap {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} :
      Coe (Lake.DRBMap α (fun (x : α) => β) cmp) (Lean.RBMap α β cmp)
      Equations
      • Lake.instCoeDRBMapRBMap = { coe := id }
      @[inline]
      def Lake.mkDRBMap (α : Type u) (β : αType v) (cmp : ααOrdering) :
      Lake.DRBMap α β cmp
      Equations
      Instances For
        @[inline]
        def Lake.DRBMap.empty {α : Type u} {β : αType v} {cmp : ααOrdering} :
        Lake.DRBMap α β cmp
        Equations
        Instances For
          instance Lake.instEmptyCollectionDRBMap (α : Type u) (β : αType v) (cmp : ααOrdering) :
          Equations
          def Lake.DRBMap.depth {α : Type u} {β : αType v} {cmp : ααOrdering} (f : NatNatNat) (t : Lake.DRBMap α β cmp) :
          Equations
          Instances For
            @[inline]
            def Lake.DRBMap.fold {α : Type u} {β : αType v} {σ : Type w} {cmp : ααOrdering} (f : σ(k : α) → β kσ) (init : σ) :
            Lake.DRBMap α β cmpσ
            Equations
            Instances For
              @[inline]
              def Lake.DRBMap.revFold {α : Type u} {β : αType v} {σ : Type w} {cmp : ααOrdering} (f : σ(k : α) → β kσ) (init : σ) :
              Lake.DRBMap α β cmpσ
              Equations
              Instances For
                @[inline]
                def Lake.DRBMap.foldM {α : Type u} {β : αType v} {σ : Type w} {cmp : ααOrdering} {m : Type w → Type u_1} [Monad m] (f : σ(k : α) → β km σ) (init : σ) :
                Lake.DRBMap α β cmpm σ
                Equations
                Instances For
                  @[inline]
                  def Lake.DRBMap.forM {α : Type u} {β : αType v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} [Monad m] (f : (k : α) → β km PUnit) (t : Lake.DRBMap α β cmp) :
                  Equations
                  Instances For
                    @[inline]
                    def Lake.DRBMap.forIn {α : Type u} {β : αType v} {σ : Type w} {cmp : ααOrdering} {m : Type w → Type u_1} [Monad m] (t : Lake.DRBMap α β cmp) (init : σ) (f : (k : α) × β kσm (ForInStep σ)) :
                    m σ
                    Equations
                    • t.forIn init f = t.val.forIn init fun (a : α) (b : β a) (acc : σ) => f a, b acc
                    Instances For
                      instance Lake.DRBMap.instForInSigma {α : Type u} {β : αType v} {cmp : ααOrdering} {m : Type u_1 → Type u_2} :
                      ForIn m (Lake.DRBMap α β cmp) ((k : α) × β k)
                      Equations
                      • Lake.DRBMap.instForInSigma = { forIn := fun {β_1 : Type ?u.38} [Monad m] => Lake.DRBMap.forIn }
                      @[inline]
                      def Lake.DRBMap.isEmpty {α : Type u} {β : αType v} {cmp : ααOrdering} :
                      Lake.DRBMap α β cmpBool
                      Equations
                      Instances For
                        @[specialize #[]]
                        def Lake.DRBMap.toList {α : Type u} {β : αType v} {cmp : ααOrdering} :
                        Lake.DRBMap α β cmpList ((k : α) × β k)
                        Equations
                        Instances For
                          @[inline]
                          def Lake.DRBMap.min {α : Type u} {β : αType v} {cmp : ααOrdering} :
                          Lake.DRBMap α β cmpOption ((k : α) × β k)
                          Equations
                          Instances For
                            @[inline]
                            def Lake.DRBMap.max {α : Type u} {β : αType v} {cmp : ααOrdering} :
                            Lake.DRBMap α β cmpOption ((k : α) × β k)
                            Equations
                            Instances For
                              instance Lake.DRBMap.instReprOfSigma {α : Type u} {β : αType v} {cmp : ααOrdering} [Repr ((k : α) × β k)] :
                              Repr (Lake.DRBMap α β cmp)
                              Equations
                              @[inline]
                              def Lake.DRBMap.insert {α : Type u} {β : αType v} {cmp : ααOrdering} :
                              Lake.DRBMap α β cmp(k : α) → β kLake.DRBMap α β cmp
                              Equations
                              Instances For
                                @[inline]
                                def Lake.DRBMap.erase {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                Lake.DRBMap α β cmpαLake.DRBMap α β cmp
                                Equations
                                Instances For
                                  @[specialize #[]]
                                  def Lake.DRBMap.ofList {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                  List ((k : α) × β k)Lake.DRBMap α β cmp
                                  Equations
                                  Instances For
                                    @[inline]
                                    def Lake.DRBMap.findCore? {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                    Lake.DRBMap α β cmpαOption ((k : α) × β k)
                                    Equations
                                    Instances For
                                      @[inline]
                                      def Lake.DRBMap.find? {α : Type u} {β : αType v} {cmp : ααOrdering} [Lake.EqOfCmpWrt α β cmp] :
                                      Lake.DRBMap α β cmp(k : α) → Option (β k)
                                      Equations
                                      Instances For
                                        @[inline]
                                        def Lake.DRBMap.findD {α : Type u} {β : αType v} {cmp : ααOrdering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) (v₀ : β k) :
                                        β k
                                        Equations
                                        • t.findD k v₀ = (t.find? k).getD v₀
                                        Instances For
                                          @[inline]
                                          def Lake.DRBMap.lowerBound {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                          Lake.DRBMap α β cmpαOption ((k : α) × β k)

                                          (lowerBound k) retrieves the kv pair of the largest key smaller than or equal to k, if it exists.

                                          Equations
                                          Instances For
                                            @[inline]
                                            def Lake.DRBMap.contains {α : Type u} {β : αType v} {cmp : ααOrdering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) :
                                            Equations
                                            • t.contains k = (t.find? k).isSome
                                            Instances For
                                              @[inline]
                                              def Lake.DRBMap.fromList {α : Type u} {β : αType v} (l : List ((k : α) × β k)) (cmp : ααOrdering) :
                                              Lake.DRBMap α β cmp
                                              Equations
                                              Instances For
                                                @[inline]
                                                def Lake.DRBMap.all {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                                Lake.DRBMap α β cmp((k : α) → β kBool)Bool
                                                Equations
                                                Instances For
                                                  @[inline]
                                                  def Lake.DRBMap.any {α : Type u} {β : αType v} {cmp : ααOrdering} :
                                                  Lake.DRBMap α β cmp((k : α) → β kBool)Bool
                                                  Equations
                                                  Instances For
                                                    def Lake.DRBMap.size {α : Type u} {β : αType v} {cmp : ααOrdering} (m : Lake.DRBMap α β cmp) :
                                                    Equations
                                                    Instances For
                                                      def Lake.DRBMap.maxDepth {α : Type u} {β : αType v} {cmp : ααOrdering} (t : Lake.DRBMap α β cmp) :
                                                      Equations
                                                      Instances For
                                                        @[inline]
                                                        def Lake.DRBMap.min! {α : Type u} {β : αType v} {cmp : ααOrdering} [Inhabited ((k : α) × β k)] (t : Lake.DRBMap α β cmp) :
                                                        (k : α) × β k
                                                        Equations
                                                        • t.min! = match t.min with | some p => p | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.min!" 136 14 "map is empty"
                                                        Instances For
                                                          @[inline]
                                                          def Lake.DRBMap.max! {α : Type u} {β : αType v} {cmp : ααOrdering} [Inhabited ((k : α) × β k)] (t : Lake.DRBMap α β cmp) :
                                                          (k : α) × β k
                                                          Equations
                                                          • t.max! = match t.max with | some p => p | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.max!" 141 14 "map is empty"
                                                          Instances For
                                                            @[inline]
                                                            def Lake.DRBMap.find! {α : Type u} {β : αType v} {cmp : ααOrdering} [Lake.EqOfCmpWrt α β cmp] (t : Lake.DRBMap α β cmp) (k : α) [Inhabited (β k)] :
                                                            β k
                                                            Equations
                                                            • t.find! k = match t.find? k with | some b => b | none => panicWithPosWithDecl "Lake.Util.DRBMap" "Lake.DRBMap.find!" 146 14 "key is not in the map"
                                                            Instances For
                                                              def Lake.drbmapOf {α : Type u} {β : αType v} (l : List ((k : α) × β k)) (cmp : ααOrdering) :
                                                              Lake.DRBMap α β cmp
                                                              Equations
                                                              Instances For