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

test: fix test

Browse source
This commit is contained in:
Sebastian Ullrich 2019-10-18 13:47:23 +02:00
parent 9b55687597
commit 9160949df3
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -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]);