summaryrefslogtreecommitdiff
path: root/tests/fstar
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/fstar/traits/Traits.fst5
1 files changed, 0 insertions, 5 deletions
diff --git a/tests/fstar/traits/Traits.fst b/tests/fstar/traits/Traits.fst
index 895a1cac..8252aad4 100644
--- a/tests/fstar/traits/Traits.fst
+++ b/tests/fstar/traits/Traits.fst
@@ -454,8 +454,3 @@ noeq type cFn_t (self args : Type0) = {
cFnMutSelfArgsInst.cFnOnceSelfArgsInst.tOutput;
}
-(** [traits::incr_u32]: forward function
- Source: 'src/traits.rs', lines 300:0-300:30 *)
-let incr_u32 (x : u32) : result u32 =
- u32_add x 1
-