Fix Hashmap and randomstate equality issue.

cryspen · Dec 17, 2024 · 6701b54 · 6701b54
1 parent 6afc8b6
commit 6701b54
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti b/proof-libs/fstar/core/Std.Collections.Hash.Map.fsti
@@ -1,5 +1,5 @@
 module Std.Collections.Hash.Map
 
-type t_HashMap (k v s:Type0)
+type t_HashMap ([@@@ strictly_positive] k [@@@ strictly_positive] v [@@@ strictly_positive] s:Type0): eqtype
 
 val impl__new #k #v: unit -> t_HashMap k v Std.Hash.Random.t_RandomState
diff --git a/proof-libs/fstar/core/Std.Hash.Random.fsti b/proof-libs/fstar/core/Std.Hash.Random.fsti
@@ -1,3 +1,3 @@
 module Std.Hash.Random
 
-type t_RandomState
+type t_RandomState: eqtype