summaryrefslogtreecommitdiff
path: root/tests/fstar/traits
diff options
context:
space:
mode:
Diffstat (limited to 'tests/fstar/traits')
-rw-r--r--tests/fstar/traits/Traits.fst2
1 files changed, 1 insertions, 1 deletions
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 3543bd73..cb9c1654 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -273,7 +273,7 @@ let use_with_const_ty1
(h : Type0) (len : usize) (withConstTyHLENInst : withConstTy_t h len) :
result usize
=
- let i = withConstTyHLENInst.cLEN1 in Return i
+ Return withConstTyHLENInst.cLEN1
(** [traits::use_with_const_ty2]:
Source: 'src/traits.rs', lines 187:0-187:73 *)