max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(init/data/default): add missing files

Browse source
This commit is contained in:
Sebastian Ullrich 2018-03-22 00:15:56 +01:00
parent 9d96f8dd62
commit 0f7a8907c7
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/data/default.lean
View file

@ -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