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