Regenerate more F* files

1 files changed, 24 insertions, 0 deletions

diff --git a/tests/fstar/array/Array.Opaque.fsti b/tests/fstar/array/Array.Opaque.fsti
new file mode 100644
index 00000000..484cb9ee
--- /dev/null
+++ b/tests/fstar/array/Array.Opaque.fsti
@@ -0,0 +1,24 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [array]: external function declarations *)
+module Array.Opaque
+open Primitives
+include Array.Types
+
+#set-options "--z3rlimit 50 --fuel 1 --ifuel 1"
+
+(** [core::array::[T; N]::{15}::index]: forward function *)
+val core_array_[T; N]_index_fwd
+  (t i : Type0) (n : usize) (inst : core_ops_index_Index (slice t) i) :
+  array t n -> i -> result inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: forward function *)
+val core_array_[T; N]_index_mut_fwd
+  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+  array t n -> i -> result inst.index_inst.core_ops_index_Index_Output
+
+(** [core::array::[T; N]::{16}::index_mut]: backward function 0 *)
+val core_array_[T; N]_index_mut_back
+  (t i : Type0) (n : usize) (inst : core_ops_index_IndexMut (slice t) i) :
+  array t n -> i -> inst.index_inst.core_ops_index_Index_Output -> result
+    (array t n)
+