blob: 484cb9ee1c52a3a1ff54c69fd8fcb75cd5ff8c65 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
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)
|
