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 2021-06-02 10:03:12 -07:00
parent 55691e2951
commit 995136d46b
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/phashmap_inst_coherence.lean
View file

@ -6,7 +6,7 @@ let m : PersistentHashMap Nat Nat := {};
m.insert 1 1
def natDiffHash : Hashable Nat :=
⟨fun n => USize.ofNat $ n+10⟩
⟨fun n => UInt64.ofNat $ n+10⟩
-- The following example should fail since the `Hashable` instance used to create `m` is not `natDiffHash`
#eval @PersistentHashMap.find? Nat Nat _ natDiffHash m 1