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

chore: fix test

Browse source
This commit is contained in:
Leonardo de Moura 2019-10-31 21:01:31 -07:00
parent b78ab05360
commit ec71dd256f
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/run/instuniv.lean
View file

@ -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 ()