diff options
author | Son Ho | 2023-11-29 11:46:35 +0100 |
---|---|---|
committer | Son Ho | 2023-11-29 11:46:35 +0100 |
commit | 59cb4312df866ec00a1fddec62a1e660b358052d (patch) | |
tree | 330092b82e591f0148c64133c14361bba3582374 | |
parent | b78850a81dfea78bc280f1b5b6d2fdcb421e386a (diff) |
Regenerate the test files
Diffstat (limited to '')
-rw-r--r-- | tests/coq/traits/Traits.v | 5 | ||||
-rw-r--r-- | tests/fstar/traits/Traits.fst | 5 | ||||
-rw-r--r-- | tests/lean/Traits.lean | 5 |
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 |