diff options
| author | Son Ho | 2023-07-05 15:17:58 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-05 15:17:58 +0200 |
| commit | 5ca36bfc50083a01af2b7ae5f75993a520757ef5 (patch) | |
| tree | 11660b73a27ad2e0807a18ac9286a1e87c560050 /tests/lean/External | |
| parent | c07721dedb2cfe4c726c42606e623395cdfe5b80 (diff) | |
Simplify the names used in Primitives.lean
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/External/Funs.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean index 10efc3db..3fc21d91 100644 --- a/tests/lean/External/Funs.lean +++ b/tests/lean/External/Funs.lean @@ -36,8 +36,8 @@ def test_new_non_zero_u32_fwd /- [external::test_vec] -/ def test_vec_fwd : Result Unit := do - let v := vec_new U32 - let _ ← vec_push_back U32 v (U32.ofInt 0 (by intlit)) + let v := Vec.new U32 + let _ ← Vec.push U32 v (U32.ofInt 0 (by intlit)) Result.ret () /- Unit test for [external::test_vec] -/ |