diff options
| author | Son Ho | 2023-12-23 00:59:55 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-23 00:59:55 +0100 |
| commit | a4decc7654bc6f3301c0174124d21fdbc2dbc708 (patch) | |
| tree | f992f3bb64609bf12d033a1424873a8134c66617 /tests/lean/External | |
| parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) | |
Regenerate the files
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/External/Funs.lean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 88ced82d..db15aacc 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -25,8 +25,7 @@ def test_new_non_zero_u32 Source: 'src/external.rs', lines 17:0-17:17 -/ def test_vec : Result Unit := do - let v := alloc.vec.Vec.new U32 - let _ ← alloc.vec.Vec.push U32 v 0#u32 + let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32 Result.ret () /- Unit test for [external::test_vec] -/ |