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/misc | |
| parent | 959d6fce38c8d8ca6eaed3ad6f458b87f91a9abc (diff) | |
Generate a dedicated file for the external types
Diffstat (limited to 'tests/fstar/misc')
| -rw-r--r-- | tests/fstar/misc/External.Types.fst | 8 | ||||
| -rw-r--r-- | tests/fstar/misc/External.TypesExternal.fsti (renamed from tests/fstar/misc/External.Types.fsti) | 4 |
2 files changed, 10 insertions, 2 deletions
diff --git a/tests/fstar/misc/External.Types.fst b/tests/fstar/misc/External.Types.fst new file mode 100644 index 00000000..4fbcec47 --- /dev/null +++ b/tests/fstar/misc/External.Types.fst @@ -0,0 +1,8 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: type definitions *) +module External.Types +open Primitives +include External.TypesExternal + +#set-options "--z3rlimit 50 --fuel 1 --ifuel 1" + diff --git a/tests/fstar/misc/External.Types.fsti b/tests/fstar/misc/External.TypesExternal.fsti index 0cb9fd0e..4bfbe0c5 100644 --- a/tests/fstar/misc/External.Types.fsti +++ b/tests/fstar/misc/External.TypesExternal.fsti @@ -1,6 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: type definitions *) -module External.Types +(** [external]: external type declarations *) +module External.TypesExternal open Primitives #set-options "--z3rlimit 50 --fuel 1 --ifuel 1" |