chore: more RBMap cleanup

This commit is contained in:
Sebastian Ullrich 2022-10-06 15:53:26 +02:00 committed by Leonardo de Moura
parent 6f4cea6dba
commit 5b7e6661f9
3 changed files with 5 additions and 5 deletions

View file

@ -6,17 +6,17 @@ Authors: Leonardo de Moura
namespace Lean
universe u v w w'
inductive Rbcolor where
inductive RBColor where
| red | black
inductive RBNode (α : Type u) (β : α → Type v) where
| leaf : RBNode α β
| node (color : Rbcolor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β
| node (color : RBColor) (lchild : RBNode α β) (key : α) (val : β key) (rchild : RBNode α β) : RBNode α β
namespace RBNode
variable {α : Type u} {β : α → Type v} {σ : Type w}
open Rbcolor Nat
open RBColor Nat
def depth (f : Nat → Nat → Nat) : RBNode α β → Nat
| leaf => 0

View file

@ -141,9 +141,9 @@
tags: [fast, suite]
run_config:
<<: *time
cmd: ./rbmap.library.lean.out 2000000
cmd: ./rbmap_library.lean.out 2000000
build_config:
cmd: ./compile.sh rbmap.library.lean
cmd: ./compile.sh rbmap_library.lean
- attributes:
description: rbmap_fbip
tags: [fast, suite]