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 2022-03-03 17:30:51 -08:00
parent 4657d47c16
commit 337c55f322
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/Array.lean
View file

@ -9,3 +9,4 @@ import Init.Data.Array.QSort
import Init.Data.Array.BinSearch
import Init.Data.Array.InsertionSort
import Init.Data.Array.DecidableEq
import Init.Data.Array.Mem