From 9160949df33684e28da90f4f528192b72f011c98 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 18 Oct 2019 13:47:23 +0200 Subject: [PATCH] test: fix test --- tests/lean/run/instuniv.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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]);