diff options
Diffstat (limited to 'tests/lean/Array')
| -rw-r--r-- | tests/lean/Array/Funs.lean | 37 |
1 files changed, 15 insertions, 22 deletions
diff --git a/tests/lean/Array/Funs.lean b/tests/lean/Array/Funs.lean index ad737dca..d3cb29d2 100644 --- a/tests/lean/Array/Funs.lean +++ b/tests/lean/Array/Funs.lean @@ -53,16 +53,6 @@ def index_array_u32 (s : Array U32 (Usize.ofInt 32)) (i : Usize) : Result U32 := Array.index_shared U32 (Usize.ofInt 32) s i -/- [array::index_array_generic]: forward function -/ -def index_array_generic - (N : Usize) (s : Array U32 N) (i : Usize) : Result U32 := - Array.index_shared U32 N s i - -/- [array::index_array_generic_call]: forward function -/ -def index_array_generic_call - (N : Usize) (s : Array U32 N) (i : Usize) : Result U32 := - index_array_generic N s i - /- [array::index_array_copy]: forward function -/ def index_array_copy (x : Array U32 (Usize.ofInt 32)) : Result U32 := Array.index_shared U32 (Usize.ofInt 32) x (Usize.ofInt 0) @@ -426,23 +416,21 @@ def f3 : Result U32 := (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) (Usize.ofInt 0) let _ ← f2 i + let b := Array.repeat U32 (Usize.ofInt 32) (U32.ofInt 0) let s ← Array.to_slice_shared U32 (Usize.ofInt 2) (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 1), (U32.ofInt 2) ]) - let s0 ← - f4 - (Array.make U32 (Usize.ofInt 32) [ - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), - (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0), (U32.ofInt 0) - ]) (Usize.ofInt 16) (Usize.ofInt 18) + let s0 ← f4 b (Usize.ofInt 16) (Usize.ofInt 18) sum2 s s0 +/- [array::SZ] -/ +def sz_body : Result Usize := Result.ret (Usize.ofInt 32) +def sz_c : Usize := eval_global sz_body (by simp) + +/- [array::f5]: forward function -/ +def f5 (x : Array U32 (Usize.ofInt 32)) : Result U32 := + Array.index_shared U32 (Usize.ofInt 32) x (Usize.ofInt 0) + /- [array::ite]: forward function -/ def ite : Result Unit := do @@ -462,4 +450,9 @@ def ite : Result Unit := (Array.make U32 (Usize.ofInt 2) [ (U32.ofInt 0), (U32.ofInt 0) ]) s2 Result.ret () +/- [array::array]: forward function -/ +def array (LEN : Usize) : Result (Array U8 LEN) := + let a := Array.repeat U8 LEN (U8.ofInt 0) + Result.ret a + end array |