From a666c7f04eb77ecfd29f253b7fc389a4507404f1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Nov 2017 19:48:35 -0800 Subject: [PATCH] chore(library/init/data/rbmap): add missing file --- library/init/data/rbmap/default.lean | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 library/init/data/rbmap/default.lean diff --git a/library/init/data/rbmap/default.lean b/library/init/data/rbmap/default.lean new file mode 100644 index 0000000000..4d5a38b69a --- /dev/null +++ b/library/init/data/rbmap/default.lean @@ -0,0 +1,7 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Leonardo de Moura +-/ +prelude +import init.data.rbtree init.data.rbmap.basic