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-06-25 11:58:49 -07:00
parent 1be221a1f4
commit 657879fcaa
5 changed files with 10 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/compiler/phashmap.lean
View file

@ -1,6 +1,6 @@
import Init.Data.PersistentHashMap
import Std.Data.PersistentHashMap
import Lean.Data.Format
open Lean PersistentHashMap
open Lean Std Std.PersistentHashMap
abbrev Map := PersistentHashMap Nat Nat

4
tests/compiler/phashmap2.lean
View file

@ -1,6 +1,6 @@
import Init.Data.PersistentHashMap
import Std.Data.PersistentHashMap
import Lean.Data.Format
open Lean PersistentHashMap
open Lean Std Std.PersistentHashMap
abbrev Map := PersistentHashMap Nat Nat

4
tests/compiler/phashmap3.lean
View file

@ -1,6 +1,6 @@
import Init.Data.PersistentHashMap
import Std.Data.PersistentHashMap
import Lean.Data.Format
open Lean PersistentHashMap
open Lean Std Std.PersistentHashMap
abbrev Map := PersistentHashMap Nat Nat

4
tests/lean/phashmap_inst_coherence.lean
View file

@ -1,5 +1,5 @@
import Init.Data.PersistentHashMap
import Std.Data.PersistentHashMap
open Std
def m : PersistentHashMap Nat Nat :=
let m : PersistentHashMap Nat Nat := {};
m.insert 1 1

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

@ -1,3 +1,5 @@
import Std.ShareCommon
open Std
def check (b : Bool) : ShareCommonT IO Unit :=
unless b $ throw $ IO.userError "check failed"