- leaf: {α : Type u} → {β : α → Type v} → Std.RBNode α β
- node: {α : Type u} → {β : α → Type v} → Std.Rbcolor → Std.RBNode α β → (key : α) → β key → Std.RBNode α β → Std.RBNode α β
Equations
- Std.RBNode.depth f Std.RBNode.leaf = 0
- Std.RBNode.depth f (Std.RBNode.node x_1 l x_2 x_3 r) = Nat.succ (f (Std.RBNode.depth f l) (Std.RBNode.depth f r))
Equations
- Std.RBNode.min Std.RBNode.leaf = none
- Std.RBNode.min (Std.RBNode.node x_1 Std.RBNode.leaf k v x_2) = some { fst := k, snd := v }
- Std.RBNode.min (Std.RBNode.node x_1 l k v x_2) = Std.RBNode.min l
Equations
- Std.RBNode.max Std.RBNode.leaf = none
- Std.RBNode.max (Std.RBNode.node x_1 x_2 k v Std.RBNode.leaf) = some { fst := k, snd := v }
- Std.RBNode.max (Std.RBNode.node x_1 x_2 k v r) = Std.RBNode.max r
@[specialize]
def
Std.RBNode.fold
{α : Type u}
{β : α → Type v}
{σ : Type w}
(f : σ → (k : α) → β k → σ)
(init : σ)
:
Std.RBNode α β → σ
Equations
- Std.RBNode.fold f x Std.RBNode.leaf = x
- Std.RBNode.fold f x (Std.RBNode.node x_2 l k v r) = Std.RBNode.fold f (f (Std.RBNode.fold f x l) k v) r
@[specialize]
def
Std.RBNode.forM
{α : Type u}
{β : α → Type v}
{m : Type → Type u_1}
[inst : Monad m]
(f : (k : α) → β k → m Unit)
:
Std.RBNode α β → m Unit
Equations
- Std.RBNode.forM f Std.RBNode.leaf = pure ()
- Std.RBNode.forM f (Std.RBNode.node x_1 l k v r) = do Std.RBNode.forM f l f k v Std.RBNode.forM f r
@[specialize]
def
Std.RBNode.foldM
{α : Type u}
{β : α → Type v}
{σ : Type w}
{m : Type w → Type u_1}
[inst : Monad m]
(f : σ → (k : α) → β k → m σ)
(init : σ)
:
Std.RBNode α β → m σ
Equations
- Std.RBNode.foldM f x Std.RBNode.leaf = pure x
- Std.RBNode.foldM f x (Std.RBNode.node x_2 l k v r) = do let b ← Std.RBNode.foldM f x l let b ← f b k v Std.RBNode.foldM f b r
@[inline]
def
Std.RBNode.forIn
{α : Type u}
{β : α → Type v}
{σ : Type w}
{m : Type w → Type u_1}
[inst : Monad m]
(as : Std.RBNode α β)
(init : σ)
(f : (k : α) → β k → σ → m (ForInStep σ))
:
m σ
Equations
- Std.RBNode.forIn as init f = (fun visit => do let a ← visit as init match a with | ForInStep.done b => pure b | ForInStep.yield b => pure b) (Std.RBNode.forIn.visit f)
@[specialize]
def
Std.RBNode.forIn.visit
{α : Type u}
{β : α → Type v}
{σ : Type w}
{m : Type w → Type u_1}
[inst : Monad m]
(f : (k : α) → β k → σ → m (ForInStep σ))
:
Std.RBNode α β → σ → m (ForInStep σ)
Equations
- Std.RBNode.forIn.visit f Std.RBNode.leaf x = pure (ForInStep.yield x)
- Std.RBNode.forIn.visit f (Std.RBNode.node x_2 l k v r) x = do let a ← Std.RBNode.forIn.visit f l x match a with | r@h:(ForInStep.done x) => pure r | ForInStep.yield b => do let a ← f k v b match a with | r@h:(ForInStep.done x) => pure r | ForInStep.yield b => Std.RBNode.forIn.visit f r b
@[specialize]
def
Std.RBNode.revFold
{α : Type u}
{β : α → Type v}
{σ : Type w}
(f : σ → (k : α) → β k → σ)
(init : σ)
:
Std.RBNode α β → σ
Equations
- Std.RBNode.revFold f x Std.RBNode.leaf = x
- Std.RBNode.revFold f x (Std.RBNode.node x_2 l k v r) = Std.RBNode.revFold f (f (Std.RBNode.revFold f x r) k v) l
@[specialize]
Equations
- Std.RBNode.all p Std.RBNode.leaf = true
- Std.RBNode.all p (Std.RBNode.node x_1 l k v r) = (p k v && Std.RBNode.all p l && Std.RBNode.all p r)
@[specialize]
Equations
- Std.RBNode.any p Std.RBNode.leaf = false
- Std.RBNode.any p (Std.RBNode.node x_1 l k v r) = (p k v || Std.RBNode.any p l || Std.RBNode.any p r)
Equations
- Std.RBNode.singleton k v = Std.RBNode.node Std.Rbcolor.red Std.RBNode.leaf k v Std.RBNode.leaf
@[inline]
def
Std.RBNode.balance1
{α : Type u}
{β : α → Type v}
(a : α)
:
β a → Std.RBNode α β → Std.RBNode α β → Std.RBNode α β
Equations
- Std.RBNode.balance1 x x x x = match x, x, x, x with | kv, vv, t, Std.RBNode.node x (Std.RBNode.node Std.Rbcolor.red l kx vx r₁) ky vy r₂ => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black l kx vx r₁) ky vy (Std.RBNode.node Std.Rbcolor.black r₂ kv vv t) | kv, vv, t, Std.RBNode.node x l₁ ky vy (Std.RBNode.node Std.Rbcolor.red l₂ kx vx r) => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black l₁ ky vy l₂) kx vx (Std.RBNode.node Std.Rbcolor.black r kv vv t) | kv, vv, t, Std.RBNode.node x l ky vy r => Std.RBNode.node Std.Rbcolor.black (Std.RBNode.node Std.Rbcolor.red l ky vy r) kv vv t | x, x_1, x_2, x_3 => Std.RBNode.leaf
@[inline]
def
Std.RBNode.balance2
{α : Type u}
{β : α → Type v}
:
(a : Std.RBNode α β) → (a : α) → β a → Std.RBNode α β → Std.RBNode α β
Equations
- Std.RBNode.balance2 x x x x = match x, x, x, x with | t, kv, vv, Std.RBNode.node x (Std.RBNode.node Std.Rbcolor.red l kx₁ vx₁ r₁) ky vy r₂ => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black t kv vv l) kx₁ vx₁ (Std.RBNode.node Std.Rbcolor.black r₁ ky vy r₂) | t, kv, vv, Std.RBNode.node x l₁ ky vy (Std.RBNode.node Std.Rbcolor.red l₂ kx₂ vx₂ r₂) => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black t kv vv l₁) ky vy (Std.RBNode.node Std.Rbcolor.black l₂ kx₂ vx₂ r₂) | t, kv, vv, Std.RBNode.node x l ky vy r => Std.RBNode.node Std.Rbcolor.black t kv vv (Std.RBNode.node Std.Rbcolor.red l ky vy r) | x, x_1, x_2, x_3 => Std.RBNode.leaf
Equations
- Std.RBNode.isRed x = match x with | Std.RBNode.node Std.Rbcolor.red x x_1 x_2 x_3 => true | x => false
Equations
- Std.RBNode.isBlack x = match x with | Std.RBNode.node Std.Rbcolor.black x x_1 x_2 x_3 => true | x => false
@[specialize]
def
Std.RBNode.ins
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
:
Std.RBNode α β → (k : α) → β k → Std.RBNode α β
Equations
- Std.RBNode.ins cmp Std.RBNode.leaf x x = Std.RBNode.node Std.Rbcolor.red Std.RBNode.leaf x x Std.RBNode.leaf
- Std.RBNode.ins cmp (Std.RBNode.node Std.Rbcolor.red a ky vy b) x x = match cmp x ky with | Ordering.lt => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.ins cmp a x x) ky vy b | Ordering.gt => Std.RBNode.node Std.Rbcolor.red a ky vy (Std.RBNode.ins cmp b x x) | Ordering.eq => Std.RBNode.node Std.Rbcolor.red a x x b
- Std.RBNode.ins cmp (Std.RBNode.node Std.Rbcolor.black a ky vy b) x x = match cmp x ky with | Ordering.lt => if Std.RBNode.isRed a = true then Std.RBNode.balance1 ky vy b (Std.RBNode.ins cmp a x x) else Std.RBNode.node Std.Rbcolor.black (Std.RBNode.ins cmp a x x) ky vy b | Ordering.gt => if Std.RBNode.isRed b = true then Std.RBNode.balance2 a ky vy (Std.RBNode.ins cmp b x x) else Std.RBNode.node Std.Rbcolor.black a ky vy (Std.RBNode.ins cmp b x x) | Ordering.eq => Std.RBNode.node Std.Rbcolor.black a x x b
Equations
- Std.RBNode.setBlack x = match x with | Std.RBNode.node x l k v r => Std.RBNode.node Std.Rbcolor.black l k v r | e => e
@[specialize]
def
Std.RBNode.insert
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
(t : Std.RBNode α β)
(k : α)
(v : β k)
:
Std.RBNode α β
Equations
- Std.RBNode.insert cmp t k v = if Std.RBNode.isRed t = true then Std.RBNode.setBlack (Std.RBNode.ins cmp t k v) else Std.RBNode.ins cmp t k v
def
Std.RBNode.balance₃
{α : Type u}
{β : α → Type v}
(a : Std.RBNode α β)
(k : α)
(v : β k)
(d : Std.RBNode α β)
:
Std.RBNode α β
Equations
- Std.RBNode.balance₃ a k v d = match a with | Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.red a kx vx b) ky vy c => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a kx vx b) ky vy (Std.RBNode.node Std.Rbcolor.black c k v d) | Std.RBNode.node Std.Rbcolor.red a kx vx (Std.RBNode.node Std.Rbcolor.red b ky vy c) => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a kx vx b) ky vy (Std.RBNode.node Std.Rbcolor.black c k v d) | a => match d with | Std.RBNode.node Std.Rbcolor.red b ky vy (Std.RBNode.node Std.Rbcolor.red c kz vz d) => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a k v b) ky vy (Std.RBNode.node Std.Rbcolor.black c kz vz d) | Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.red b ky vy c) kz vz d => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a k v b) ky vy (Std.RBNode.node Std.Rbcolor.black c kz vz d) | x => Std.RBNode.node Std.Rbcolor.black a k v d
Equations
- Std.RBNode.setRed x = match x with | Std.RBNode.node x a k v b => Std.RBNode.node Std.Rbcolor.red a k v b | e => e
def
Std.RBNode.balLeft
{α : Type u}
{β : α → Type v}
:
Std.RBNode α β → (k : α) → β k → Std.RBNode α β → Std.RBNode α β
Equations
- Std.RBNode.balLeft x x x x = match x, x, x, x with | Std.RBNode.node Std.Rbcolor.red a kx vx b, k, v, r => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a kx vx b) k v r | l, k, v, Std.RBNode.node Std.Rbcolor.black a ky vy b => Std.RBNode.balance₃ l k v (Std.RBNode.node Std.Rbcolor.red a ky vy b) | l, k, v, Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black a ky vy b) kz vz c => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.node Std.Rbcolor.black l k v a) ky vy (Std.RBNode.balance₃ b kz vz (Std.RBNode.setRed c)) | l, k, v, r => Std.RBNode.node Std.Rbcolor.red l k v r
def
Std.RBNode.balRight
{α : Type u}
{β : α → Type v}
(l : Std.RBNode α β)
(k : α)
(v : β k)
(r : Std.RBNode α β)
:
Std.RBNode α β
Equations
- Std.RBNode.balRight l k v r = match r with | Std.RBNode.node Std.Rbcolor.red b ky vy c => Std.RBNode.node Std.Rbcolor.red l k v (Std.RBNode.node Std.Rbcolor.black b ky vy c) | x => match l with | Std.RBNode.node Std.Rbcolor.black a kx vx b => Std.RBNode.balance₃ (Std.RBNode.node Std.Rbcolor.red a kx vx b) k v r | Std.RBNode.node Std.Rbcolor.red a kx vx (Std.RBNode.node Std.Rbcolor.black b ky vy c) => Std.RBNode.node Std.Rbcolor.red (Std.RBNode.balance₃ (Std.RBNode.setRed a) kx vx b) ky vy (Std.RBNode.node Std.Rbcolor.black c k v r) | x => Std.RBNode.node Std.Rbcolor.red l k v r
partial def
Std.RBNode.appendTrees
{α : Type u}
{β : α → Type v}
:
Std.RBNode α β → Std.RBNode α β → Std.RBNode α β
@[specialize]
def
Std.RBNode.del
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
(x : α)
:
Std.RBNode α β → Std.RBNode α β
Equations
- Std.RBNode.del cmp x Std.RBNode.leaf = Std.RBNode.leaf
- Std.RBNode.del cmp x (Std.RBNode.node x_2 l k v r) = match cmp x k with | Ordering.lt => if Std.RBNode.isBlack l = true then Std.RBNode.balLeft (Std.RBNode.del cmp x l) k v r else Std.RBNode.node Std.Rbcolor.red (Std.RBNode.del cmp x l) k v r | Ordering.gt => if Std.RBNode.isBlack r = true then Std.RBNode.balRight l k v (Std.RBNode.del cmp x r) else Std.RBNode.node Std.Rbcolor.red l k v (Std.RBNode.del cmp x r) | Ordering.eq => Std.RBNode.appendTrees l r
@[specialize]
def
Std.RBNode.erase
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
(x : α)
(t : Std.RBNode α β)
:
Std.RBNode α β
Equations
- Std.RBNode.erase cmp x t = let t := Std.RBNode.del cmp x t; Std.RBNode.setBlack t
@[specialize]
def
Std.RBNode.findCore
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
:
Std.RBNode α β → (k : α) → Option ((k : α) × β k)
Equations
- Std.RBNode.findCore cmp Std.RBNode.leaf x = none
- Std.RBNode.findCore cmp (Std.RBNode.node x_2 a ky vy b) x = match cmp x ky with | Ordering.lt => Std.RBNode.findCore cmp a x | Ordering.gt => Std.RBNode.findCore cmp b x | Ordering.eq => some { fst := ky, snd := vy }
@[specialize]
def
Std.RBNode.find
{α : Type u}
(cmp : α → α → Ordering)
{β : Type v}
:
(Std.RBNode α fun x => β) → α → Option β
Equations
- Std.RBNode.find cmp Std.RBNode.leaf x = none
- Std.RBNode.find cmp (Std.RBNode.node x_2 a ky vy b) x = match cmp x ky with | Ordering.lt => Std.RBNode.find cmp a x | Ordering.gt => Std.RBNode.find cmp b x | Ordering.eq => some vy
@[specialize]
def
Std.RBNode.lowerBound
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
:
Std.RBNode α β → α → Option (Sigma β) → Option (Sigma β)
Equations
- Std.RBNode.lowerBound cmp Std.RBNode.leaf x x = x
- Std.RBNode.lowerBound cmp (Std.RBNode.node x_3 a ky vy b) x x = match cmp x ky with | Ordering.lt => Std.RBNode.lowerBound cmp a x x | Ordering.gt => Std.RBNode.lowerBound cmp b x (some { fst := ky, snd := vy }) | Ordering.eq => some { fst := ky, snd := vy }
inductive
Std.RBNode.WellFormed
{α : Type u}
{β : α → Type v}
(cmp : α → α → Ordering)
:
Std.RBNode α β → Prop
- leafWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering}, Std.RBNode.WellFormed cmp Std.RBNode.leaf
- insertWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : Std.RBNode α β} {k : α} {v : β k}, Std.RBNode.WellFormed cmp n → n' = Std.RBNode.insert cmp n k v → Std.RBNode.WellFormed cmp n'
- eraseWff: ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {n n' : Std.RBNode α β} {k : α}, Std.RBNode.WellFormed cmp n → n' = Std.RBNode.erase cmp k n → Std.RBNode.WellFormed cmp n'
@[inline]
Equations
- Std.mkRBMap α β cmp = { val := Std.RBNode.leaf, property := (_ : Std.RBNode.WellFormed cmp Std.RBNode.leaf) }
@[inline]
Equations
- Std.RBMap.empty = Std.mkRBMap α β cmp
instance
Std.instEmptyCollectionRBMap
(α : Type u)
(β : Type v)
(cmp : α → α → Ordering)
:
EmptyCollection (Std.RBMap α β cmp)
Equations
- Std.instEmptyCollectionRBMap α β cmp = { emptyCollection := Std.RBMap.empty }
def
Std.RBMap.depth
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
(f : Nat → Nat → Nat)
(t : Std.RBMap α β cmp)
:
Equations
- Std.RBMap.depth f t = Std.RBNode.depth f t.val
@[inline]
def
Std.RBMap.fold
{α : Type u}
{β : Type v}
{σ : Type w}
{cmp : α → α → Ordering}
(f : σ → α → β → σ)
(init : σ)
:
Std.RBMap α β cmp → σ
Equations
- Std.RBMap.fold f x x = match x, x with | b, { val := t, property := x } => Std.RBNode.fold f b t
@[inline]
def
Std.RBMap.revFold
{α : Type u}
{β : Type v}
{σ : Type w}
{cmp : α → α → Ordering}
(f : σ → α → β → σ)
(init : σ)
:
Std.RBMap α β cmp → σ
Equations
- Std.RBMap.revFold f x x = match x, x with | b, { val := t, property := x } => Std.RBNode.revFold f b t
@[inline]
def
Std.RBMap.foldM
{α : Type u}
{β : Type v}
{σ : Type w}
{cmp : α → α → Ordering}
{m : Type w → Type u_1}
[inst : Monad m]
(f : σ → α → β → m σ)
(init : σ)
:
Std.RBMap α β cmp → m σ
Equations
- Std.RBMap.foldM f x x = match x, x with | b, { val := t, property := x } => Std.RBNode.foldM f b t
@[inline]
def
Std.RBMap.forM
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
{m : Type u_1 → Type u_2}
[inst : Monad m]
(f : α → β → m PUnit)
(t : Std.RBMap α β cmp)
:
m PUnit
Equations
- Std.RBMap.forM f t = Std.RBMap.foldM (fun x k v => f k v) PUnit.unit t
@[inline]
def
Std.RBMap.forIn
{α : Type u}
{β : Type v}
{σ : Type w}
{cmp : α → α → Ordering}
{m : Type w → Type u_1}
[inst : Monad m]
(t : Std.RBMap α β cmp)
(init : σ)
(f : α × β → σ → m (ForInStep σ))
:
m σ
Equations
- Std.RBMap.forIn t init f = Std.RBNode.forIn t.val init fun a b acc => f (a, b) acc
@[inline]
Equations
- Std.RBMap.isEmpty x = match x with | { val := Std.RBNode.leaf, property := x } => true | x => false
@[specialize]
Equations
- Std.RBMap.toList x = match x with | { val := t, property := x } => Std.RBNode.revFold (fun ps k v => (k, v) :: ps) [] t
@[inline]
Equations
- Std.RBMap.min x = match x with | { val := t, property := x } => match Std.RBNode.min t with | some { fst := k, snd := v } => some (k, v) | none => none
@[inline]
Equations
- Std.RBMap.max x = match x with | { val := t, property := x } => match Std.RBNode.max t with | some { fst := k, snd := v } => some (k, v) | none => none
instance
Std.RBMap.instReprRBMap
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[inst : Repr α]
[inst : Repr β]
:
Equations
- Std.RBMap.instReprRBMap = { reprPrec := fun m prec => Repr.addAppParen (Std.Format.text "Std.rbmapOf " ++ repr (Std.RBMap.toList m)) prec }
@[inline]
Equations
- Std.RBMap.insert x x x = match x, x, x with | { val := t, property := w }, k, v => { val := Std.RBNode.insert cmp t k v, property := (_ : Std.RBNode.WellFormed cmp (Std.RBNode.insert cmp t k v)) }
@[inline]
Equations
- Std.RBMap.erase x x = match x, x with | { val := t, property := w }, k => { val := Std.RBNode.erase cmp k t, property := (_ : Std.RBNode.WellFormed cmp (Std.RBNode.erase cmp k t)) }
@[specialize]
Equations
- Std.RBMap.ofList [] = Std.mkRBMap α β cmp
- Std.RBMap.ofList ((k, v) :: xs) = Std.RBMap.insert (Std.RBMap.ofList xs) k v
@[inline]
Equations
- Std.RBMap.findCore? x x = match x, x with | { val := t, property := x }, x_1 => Std.RBNode.findCore cmp t x_1
@[inline]
Equations
- Std.RBMap.find? x x = match x, x with | { val := t, property := x }, x_1 => Std.RBNode.find cmp t x_1
@[inline]
def
Std.RBMap.findD
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
(t : Std.RBMap α β cmp)
(k : α)
(v₀ : β)
:
β
Equations
- Std.RBMap.findD t k v₀ = Option.getD (Std.RBMap.find? t k) v₀
@[inline]
Equations
- Std.RBMap.lowerBound x x = match x, x with | { val := t, property := x }, x_1 => Std.RBNode.lowerBound cmp t x_1 none
@[inline]
def
Std.RBMap.contains
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
(t : Std.RBMap α β cmp)
(a : α)
:
Equations
- Std.RBMap.contains t a = Option.isSome (Std.RBMap.find? t a)
@[inline]
def
Std.RBMap.fromList
{α : Type u}
{β : Type v}
(l : List (α × β))
(cmp : α → α → Ordering)
:
Std.RBMap α β cmp
Equations
- Std.RBMap.fromList l cmp = List.foldl (fun r p => Std.RBMap.insert r p.fst p.snd) (Std.mkRBMap α β cmp) l
@[inline]
Equations
- Std.RBMap.all x x = match x, x with | { val := t, property := x }, p => Std.RBNode.all p t
@[inline]
Equations
- Std.RBMap.any x x = match x, x with | { val := t, property := x }, p => Std.RBNode.any p t
Equations
- Std.RBMap.size m = Std.RBMap.fold (fun sz x x => sz + 1) 0 m
Equations
- Std.RBMap.maxDepth t = Std.RBNode.depth Nat.max t.val
@[inline]
def
Std.RBMap.min!
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[inst : Inhabited α]
[inst : Inhabited β]
(t : Std.RBMap α β cmp)
:
α × β
Equations
- Std.RBMap.min! t = match Std.RBMap.min t with | some p => p | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.min!" 337 14 "map is empty"
@[inline]
def
Std.RBMap.max!
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[inst : Inhabited α]
[inst : Inhabited β]
(t : Std.RBMap α β cmp)
:
α × β
Equations
- Std.RBMap.max! t = match Std.RBMap.max t with | some p => p | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.max!" 342 14 "map is empty"
@[inline]
def
Std.RBMap.find!
{α : Type u}
{β : Type v}
{cmp : α → α → Ordering}
[inst : Inhabited β]
(t : Std.RBMap α β cmp)
(k : α)
:
β
Equations
- Std.RBMap.find! t k = match Std.RBMap.find? t k with | some b => b | none => panicWithPosWithDecl "Std.Data.RBMap" "Std.RBMap.find!" 347 14 "key is not in the map"
def
Std.rbmapOf
{α : Type u}
{β : Type v}
(l : List (α × β))
(cmp : α → α → Ordering)
:
Std.RBMap α β cmp
Equations
- Std.rbmapOf l cmp = Std.RBMap.fromList l cmp