From 0f7a8907c7167ee16e23f59b32bcfca84122fd40 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 22 Mar 2018 00:15:56 +0100 Subject: [PATCH] fix(init/data/default): add missing files --- library/init/data/default.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/default.lean b/library/init/data/default.lean index a2b496e9cd..b594f46583 100644 --- a/library/init/data/default.lean +++ b/library/init/data/default.lean @@ -7,4 +7,4 @@ prelude import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string import init.data.list init.data.sum init.data.subtype init.data.int init.data.array import init.data.bool init.data.fin init.data.unsigned init.data.ordering -import init.data.rbtree init.data.rbmap +import init.data.rbtree init.data.rbmap init.data.option.basic init.data.option.instances