diff options
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/array/Array_Funs.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/tests/coq/array/Array_Funs.v b/tests/coq/array/Array_Funs.v index d47e4633..6ff3066a 100644 --- a/tests/coq/array/Array_Funs.v +++ b/tests/coq/array/Array_Funs.v @@ -451,6 +451,15 @@ Definition f3_fwd (n : nat) : result u32 := sum2_fwd n s s0 . +(** [array::SZ] *) +Definition sz_body : result usize := Return 32%usize. +Definition sz_c : usize := sz_body%global. + +(** [array::f5]: forward function *) +Definition f5_fwd (x : array u32 32%usize) : result u32 := + array_index_shared u32 32%usize x 0%usize +. + (** [array::ite]: forward function *) Definition ite_fwd : result unit := s <- |