diff options
| -rw-r--r-- | tests/lean/External/FunsExternal.lean | 17 |
1 files changed, 3 insertions, 14 deletions
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean index aae11ba1..63830abc 100644 --- a/tests/lean/External/FunsExternal.lean +++ b/tests/lean/External/FunsExternal.lean @@ -8,22 +8,11 @@ open external /- [core::mem::swap] -/ def core.mem.swap - (T : Type) : T → T → State → Result (State × Unit) := - fun _x _y s => .ret (s, ()) - -/- [core::mem::swap] -/ -def core.mem.swap_back0 - (T : Type) : T → T → State → State → Result (State × T) := - fun _x y _s0 s1 => .ret (s1, y) - -/- [core::mem::swap] -/ -def core.mem.swap_back1 - (T : Type) : T → T → State → State → Result (State × T) := - fun x _y _s0 s1 => .ret (s1, x) + (T : Type) : T → T → State → Result (State × (T × T)) := + fun x y s => .ret (s, (y, x)) /- [core::num::nonzero::NonZeroU32::{14}::new] -/ -def core.num.nonzero.NonZeroU32.new - : +def core.num.nonzero.NonZeroU32.new : U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) := fun _ _ => .fail .panic |