diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean index 6c24a6fe6c..09c5cdcb65 100644 --- a/tests/lean/run/instuniv.lean +++ b/tests/lean/run/instuniv.lean @@ -2,7 +2,7 @@ import Init.Lean open Lean def tst : IO Unit := -do env ← importModules [`init.data.array.default]; +do env ← importModules [`Init.Data.Array.Default]; match env.find `Array.foldl with | some info => do IO.println (info.instantiateTypeUnivParams [Level.zero, Level.zero]);