diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.Types.fst (renamed from tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti) | 4 | ||||
| -rw-r--r-- | tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti | 10 |
2 files changed, 11 insertions, 3 deletions
diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst index e77954ad..afebcde3 100644 --- a/tests/fstar/hashmap_on_disk/HashmapMain.Types.fsti +++ b/tests/fstar/hashmap_on_disk/HashmapMain.Types.fst @@ -2,6 +2,7 @@ (** [hashmap_main]: type definitions *) module HashmapMain.Types open Primitives +include HashmapMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -21,6 +22,3 @@ type hashmap_HashMap_t (t : Type0) = slots : alloc_vec_Vec (hashmap_List_t t); } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti new file mode 100644 index 00000000..75747408 --- /dev/null +++ b/tests/fstar/hashmap_on_disk/HashmapMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [hashmap_main]: external type declarations *) +module HashmapMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + |