diff options
| author | Son Ho | 2023-11-27 10:29:25 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-27 10:29:25 +0100 |
| commit | bef2bd34fcb0817f1b7d16b95122bcc3c6f05c72 (patch) | |
| tree | b491462e77665dceb44b4899f97508d440c57d6a /tests/fstar/betree | |
| parent | 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (diff) | |
Generate a dedicated file for the external types
Diffstat (limited to '')
| -rw-r--r-- | tests/fstar/betree/BetreeMain.Types.fst (renamed from tests/fstar/betree/BetreeMain.Types.fsti) | 4 | ||||
| -rw-r--r-- | tests/fstar/betree/BetreeMain.TypesExternal.fsti | 10 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.Types.fst (renamed from tests/fstar/betree_back_stateful/BetreeMain.Types.fsti) | 4 | ||||
| -rw-r--r-- | tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti | 10 |
4 files changed, 22 insertions, 6 deletions
diff --git a/tests/fstar/betree/BetreeMain.Types.fsti b/tests/fstar/betree/BetreeMain.Types.fst index a098ec19..b87219b2 100644 --- a/tests/fstar/betree/BetreeMain.Types.fsti +++ b/tests/fstar/betree/BetreeMain.Types.fst @@ -2,6 +2,7 @@ (** [betree_main]: type definitions *) module BetreeMain.Types open Primitives +include BetreeMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -58,6 +59,3 @@ type betree_BeTree_t = root : betree_Node_t; } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree/BetreeMain.TypesExternal.fsti b/tests/fstar/betree/BetreeMain.TypesExternal.fsti new file mode 100644 index 00000000..1b2c53a6 --- /dev/null +++ b/tests/fstar/betree/BetreeMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external type declarations *) +module BetreeMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + diff --git a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst index a098ec19..b87219b2 100644 --- a/tests/fstar/betree_back_stateful/BetreeMain.Types.fsti +++ b/tests/fstar/betree_back_stateful/BetreeMain.Types.fst @@ -2,6 +2,7 @@ (** [betree_main]: type definitions *) module BetreeMain.Types open Primitives +include BetreeMain.TypesExternal #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" @@ -58,6 +59,3 @@ type betree_BeTree_t = root : betree_Node_t; } -(** The state type used in the state-error monad *) -val state : Type0 - diff --git a/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti new file mode 100644 index 00000000..1b2c53a6 --- /dev/null +++ b/tests/fstar/betree_back_stateful/BetreeMain.TypesExternal.fsti @@ -0,0 +1,10 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [betree_main]: external type declarations *) +module BetreeMain.TypesExternal +open Primitives + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + +(** The state type used in the state-error monad *) +val state : Type0 + |