diff options
| author | Son Ho | 2024-02-02 23:16:57 +0100 |
|---|---|---|
| committer | Son Ho | 2024-02-02 23:16:57 +0100 |
| commit | 63ee3b1bc65b67aeed843f052d7f67c9f3c0ab89 (patch) | |
| tree | 988e7fc35064910e56d4a510465f5172b8828da0 /tests/lean/Traits.lean | |
| parent | 1259db13a154b0d5f101d2f874ae017b81ed4e72 (diff) | |
Start fixing the tests
Diffstat (limited to 'tests/lean/Traits.lean')
| -rw-r--r-- | tests/lean/Traits.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean index d32aba86..3ef4febc 100644 --- a/tests/lean/Traits.lean +++ b/tests/lean/Traits.lean @@ -249,7 +249,7 @@ def traits.ToTypetraitsBoolWrapperTInst (T : Type) (ToTypeBoolTInst : ToType Source: 'src/traits.rs', lines 164:4-164:21 -/ def with_const_ty_len2_body : Result Usize := Result.ret 32#usize def with_const_ty_len2_c : Usize := - eval_global with_const_ty_len2_body (by simp) + eval_global with_const_ty_len2_body (by decide) /- Trait declaration: [traits::WithConstTy] Source: 'src/traits.rs', lines 161:0-161:39 -/ @@ -264,7 +264,7 @@ structure WithConstTy (Self : Type) (LEN : Usize) where /- [traits::{bool#8}::LEN1] Source: 'src/traits.rs', lines 175:4-175:21 -/ def bool_len1_body : Result Usize := Result.ret 12#usize -def bool_len1_c : Usize := eval_global bool_len1_body (by simp) +def bool_len1_c : Usize := eval_global bool_len1_body (by decide) /- [traits::{bool#8}::f]: Source: 'src/traits.rs', lines 180:4-180:39 -/ |