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

chore: fix tests

Browse source
This commit is contained in:
Leonardo de Moura 2020-11-20 17:00:13 -08:00
parent 8dfb0324c5
commit fa6d35adfa
2 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
tests/lean/run/instances.lean
View file

@ -5,7 +5,9 @@ open Lean.Meta
unsafe def tst1 : IO Unit :=
withImportModules [{module := `Lean}] {} 0 fun env => do
let insts := env.getGlobalInstances;
IO.println (format insts)
let aux : MetaM Unit := do
let insts ← getGlobalInstancesIndex
IO.println (format insts)
discard <| aux.run |>.toIO {} { env := env }
#eval tst1

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

@ -233,7 +233,7 @@ do print "----- tst14 -----";
let stateM ← mkStateM nat;
print stateM;
let monad ← mkMonad stateM;
let globalInsts ← getGlobalInstances;
let globalInsts ← getGlobalInstancesIndex;
let insts ← globalInsts.getUnify monad;
print insts;
pure ()