summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2023-11-29 11:46:35 +0100
committerSon Ho2023-11-29 11:46:35 +0100
commit59cb4312df866ec00a1fddec62a1e660b358052d (patch)
tree330092b82e591f0148c64133c14361bba3582374
parentb78850a81dfea78bc280f1b5b6d2fdcb421e386a (diff)
Regenerate the test files
Diffstat (limited to '')
-rw-r--r--tests/coq/traits/Traits.v5
-rw-r--r--tests/fstar/traits/Traits.fst5
-rw-r--r--tests/lean/Traits.lean5
3 files changed, 0 insertions, 15 deletions
diff --git a/tests/coq/traits/Traits.v b/tests/coq/traits/Traits.v
index ebdca4ec..549a7116 100644
--- a/tests/coq/traits/Traits.v
+++ b/tests/coq/traits/Traits.v
@@ -606,9 +606,4 @@ Arguments mkCFn_t { _ _ }.
Arguments CFn_tCFn_t_CFnMutSelfArgsInst { _ _ }.
Arguments CFn_t_call_mut { _ _ }.
-(** [traits::incr_u32]: forward function
- Source: 'src/traits.rs', lines 300:0-300:30 *)
-Definition incr_u32 (x : u32) : result u32 :=
- u32_add x 1%u32.
-
End Traits.
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
-
diff --git a/tests/lean/Traits.lean b/tests/lean/Traits.lean
index e7795d9c..653384d6 100644
--- a/tests/lean/Traits.lean
+++ b/tests/lean/Traits.lean
@@ -468,9 +468,4 @@ structure CFn (Self Args : Type) where
call_mut : Self → Args → Result
CFnMutSelfArgsInst.CFnOnceSelfArgsInst.Output
-/- [traits::incr_u32]: forward function
- Source: 'src/traits.rs', lines 300:0-300:30 -/
-def incr_u32 (x : U32) : Result U32 :=
- x + 1#u32
-
end traits