diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean index 09c5cdcb65..65c3bc3d83 100644 --- a/tests/lean/run/instuniv.lean +++ b/tests/lean/run/instuniv.lean @@ -5,8 +5,8 @@ def tst : IO Unit := do env ← importModules [`Init.Data.Array.Default]; match env.find `Array.foldl with | some info => do - IO.println (info.instantiateTypeUnivParams [Level.zero, Level.zero]); - IO.println (info.instantiateValueUnivParams [Level.zero, Level.zero]); + IO.println (info.instantiateTypeLevelParams [Level.zero, Level.zero]); + IO.println (info.instantiateValueLevelParams [Level.zero, Level.zero]); pure () | none => IO.println ("Array.foldl not found"); pure ()