From 6fd112a30d12cda6390ea3b856a81096d6bcedfe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 00:17:07 +0100
Subject: Fix a minor issue in the Lean tests

---
 tests/lean/External/FunsExternal.lean | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

(limited to 'tests/lean/External')

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
 
-- 
cgit v1.2.3