diff --git a/src/Lean/Data/RBMap.lean b/src/Lean/Data/RBMap.lean index 22221ec697..6b235c260e 100644 --- a/src/Lean/Data/RBMap.lean +++ b/src/Lean/Data/RBMap.lean @@ -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 diff --git a/tests/bench/rbmap.library.lean b/tests/bench/rbmap_library.lean similarity index 100% rename from tests/bench/rbmap.library.lean rename to tests/bench/rbmap_library.lean diff --git a/tests/bench/speedcenter.exec.velcom.yaml b/tests/bench/speedcenter.exec.velcom.yaml index b97607c67c..ece2ab9154 100644 --- a/tests/bench/speedcenter.exec.velcom.yaml +++ b/tests/bench/speedcenter.exec.velcom.yaml @@ -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]