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/Traits.lean | |
| parent | ff9fe8aa1e13a7297f7c4f2c2554235361db038f (diff) | |
Regenerate the files
Diffstat (limited to 'tests/lean/Traits.lean')
| -rw-r--r-- | tests/lean/Traits.lean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index 63d07d85..35f9e5bf 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -288,8 +288,7 @@ def use_with_const_ty1 (H : Type) (LEN : Usize) (WithConstTyHLENInst : WithConstTy H LEN) : Result Usize := - let i := WithConstTyHLENInst.LEN1 - Result.ret i + Result.ret WithConstTyHLENInst.LEN1 /- [traits::use_with_const_ty2]: Source: 'src/traits.rs', lines 187:0-187:73 -/ |