From 703261b6c8ad680a925ae0550117a85d9dfa40fe Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 25 Apr 2024 13:42:23 +0200
Subject: Update the tests for External

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

(limited to 'tests/lean/External/FunsExternal.lean')

diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index b6efc65f..28ba2077 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -4,19 +4,14 @@ import External.Types
 open Primitives
 open external
 
--- TODO: fill those bodies
+/- [core::cell::{core::cell::Cell<T>#10}::get]: -/
+def core.cell.Cell.get
+  (T : Type) (markerCopyInst : core.marker.Copy T) (c : core.cell.Cell T) (s : State) :
+  Result (State × T) :=
+  sorry
 
-/- [core::mem::swap] -/
-def core.mem.swap
-  (T : Type) : T → T → State → Result (State × (T × T)) :=
-  fun x y s => .ok (s, (y, x))
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]: -/
+def core.cell.Cell.get_mut (T : Type) (c : core.cell.Cell T) (s : State) :
+  Result (State × (T × (T → State → Result (State × (core.cell.Cell T))))) :=
+  sorry
 
-/- [core::num::nonzero::NonZeroU32::{14}::new] -/
-def core.num.nonzero.NonZeroU32.new :
-  U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) :=
-  fun _ _ => .fail .panic
-
-/- [core::option::Option::{0}::unwrap] -/
-def core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T) :=
-  fun _ _ => .fail .panic
-- 
cgit v1.2.3