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

fix: missing import

Browse source
This commit is contained in:
Leonardo de Moura 2020-06-25 11:20:47 -07:00
parent 81376d3902
commit decab1ea57
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Init/Data.lean
View file

@ -11,6 +11,7 @@ import Init.Data.String
import Init.Data.List
import Init.Data.Int
import Init.Data.Array
import Init.Data.PersistentArray
import Init.Data.ByteArray
import Init.Data.FloatArray
import Init.Data.Fin