6 files changed, 66 insertions, 83 deletions
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 78e0f95c..20c4b8e5 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -7,58 +7,28 @@ open Primitives
 
 namespace external
 
-/- [external::swap]:
-   Source: 'src/external.rs', lines 6:0-6:46 -/
-def swap
-  (T : Type) (x : T) (y : T) (st : State) : Result (State × (T × T)) :=
-  core.mem.swap T x y st
-
-/- [external::test_new_non_zero_u32]:
-   Source: 'src/external.rs', lines 11:0-11:60 -/
-def test_new_non_zero_u32
-  (x : U32) (st : State) : Result (State × core.num.nonzero.NonZeroU32) :=
-  do
-  let (st1, o) ← core.num.nonzero.NonZeroU32.new x st
-  core.option.Option.unwrap core.num.nonzero.NonZeroU32 o st1
-
-/- [external::test_vec]:
-   Source: 'src/external.rs', lines 17:0-17:17 -/
-def test_vec : Result Unit :=
-  do
-  let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
-  Result.ok ()
-
-/- Unit test for [external::test_vec] -/
-#assert (test_vec == Result.ok ())
-
-/- [external::custom_swap]:
-   Source: 'src/external.rs', lines 24:0-24:66 -/
-def custom_swap
-  (T : Type) (x : T) (y : T) (st : State) :
-  Result (State × (T × (T → State → Result (State × (T × T)))))
+/- Trait implementation: [core::marker::{(core::marker::Copy for u32)#40}]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 47:29-47:65
+   Name pattern: core::marker::Copy<u32> -/
+def core.marker.CopyU32 : core.marker.Copy U32 := {
+  cloneCloneInst := core.clone.CloneU32
+}
+
+/- [external::use_get]:
+   Source: 'src/external.rs', lines 5:0-5:37 -/
+def use_get (rc : core.cell.Cell U32) (st : State) : Result (State × U32) :=
+  core.cell.Cell.get U32 core.marker.CopyU32 rc st
+
+/- [external::incr]:
+   Source: 'src/external.rs', lines 9:0-9:31 -/
+def incr
+  (rc : core.cell.Cell U32) (st : State) :
+  Result (State × (core.cell.Cell U32))
   :=
   do
-  let (st1, (x1, y1)) ← core.mem.swap T x y st
-  let back := fun ret st2 => Result.ok (st2, (ret, y1))
-  Result.ok (st1, (x1, back))
-
-/- [external::test_custom_swap]:
-   Source: 'src/external.rs', lines 29:0-29:59 -/
-def test_custom_swap
-  (x : U32) (y : U32) (st : State) : Result (State × (U32 × U32)) :=
-  do
-  let (st1, (_, custom_swap_back)) ← custom_swap U32 x y st
-  let (_, (x1, y1)) ← custom_swap_back 1#u32 st1
-  Result.ok (st1, (x1, y1))
-
-/- [external::test_swap_non_zero]:
-   Source: 'src/external.rs', lines 35:0-35:44 -/
-def test_swap_non_zero (x : U32) (st : State) : Result (State × U32) :=
-  do
-  let (st1, p) ← swap U32 x 0#u32 st
-  let (x1, _) := p
-  if x1 = 0#u32
-  then Result.fail .panic
-  else Result.ok (st1, x1)
+  let (st1, (i, get_mut_back)) ← core.cell.Cell.get_mut U32 rc st
+  let i1 ← i + 1#u32
+  let (_, rc1) ← get_mut_back i1 st1
+  Result.ok (st1, rc1)
 
 end external
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
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean
index f0e771f7..a6163c96 100644
--- a/tests/lean/External/FunsExternal_Template.lean
+++ b/tests/lean/External/FunsExternal_Template.lean
@@ -6,15 +6,18 @@ import External.Types
 open Primitives
 open external
 
-/- [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57
-   Name pattern: core::num::nonzero::{core::num::nonzero::NonZeroU32}::new -/
-axiom core.num.nonzero.NonZeroU32.new
-  : U32 → State → Result (State × (Option core.num.nonzero.NonZeroU32))
+/- [core::cell::{core::cell::Cell<T>#10}::get]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 497:4-497:26
+   Name pattern: core::cell::{core::cell::Cell<@T>}::get -/
+axiom core.cell.Cell.get
+  (T : Type) (markerCopyInst : core.marker.Copy T) :
+  core.cell.Cell T → State → Result (State × T)
 
-/- [core::option::{core::option::Option<T>}::unwrap]:
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34
-   Name pattern: core::option::{core::option::Option<@T>}::unwrap -/
-axiom core.option.Option.unwrap
-  (T : Type) : Option T → State → Result (State × T)
+/- [core::cell::{core::cell::Cell<T>#11}::get_mut]:
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 574:4-574:39
+   Name pattern: core::cell::{core::cell::Cell<@T>}::get_mut -/
+axiom core.cell.Cell.get_mut
+  (T : Type) :
+  core.cell.Cell T → State → Result (State × (T × (T → State → Result
+    (State × (core.cell.Cell T)))))
 
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index 961f3e8a..5d4cfc77 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -6,4 +6,10 @@ open Primitives
 
 namespace external
 
+/- Trait declaration: [core::marker::Copy]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/marker.rs', lines 450:0-450:21
+   Name pattern: core::marker::Copy -/
+structure core.marker.Copy (Self : Type) where
+  cloneCloneInst : core.clone.Clone Self
+
 end external
diff --git a/tests/lean/External/TypesExternal.lean b/tests/lean/External/TypesExternal.lean
index 7c30f792..d0f5a0cc 100644
--- a/tests/lean/External/TypesExternal.lean
+++ b/tests/lean/External/TypesExternal.lean
@@ -1,11 +1,20 @@
 -- [external]: external types.
 import Base
-open Primitives
+open Lean Primitives
 
 /- [core::num::nonzero::NonZeroU32]
    Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+structure core.cell.Cell (T : Type) :=
+  id : Nat
 
-/- The state type used in the state-error monad -/
-axiom State : Type
+def CellValue := (T:Type) × T
+
+/- The state type used in the state-error monad
 
+   TODO: we tried the following definition, but it makes State a Type 1, leading
+   to type errors later:
+
+     structure State :=
+       cells : AssocList Nat CellValue
+  -/
+axiom State : Type
diff --git a/tests/lean/External/TypesExternal_Template.lean b/tests/lean/External/TypesExternal_Template.lean
index 84245531..2e6ed6e0 100644
--- a/tests/lean/External/TypesExternal_Template.lean
+++ b/tests/lean/External/TypesExternal_Template.lean
@@ -4,10 +4,10 @@
 import Base
 open Primitives
 
-/- [core::num::nonzero::NonZeroU32]
-   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 50:12-50:33
-   Name pattern: core::num::nonzero::NonZeroU32 -/
-axiom core.num.nonzero.NonZeroU32 : Type
+/- [core::cell::Cell]
+   Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/cell.rs', lines 293:0-293:26
+   Name pattern: core::cell::Cell -/
+axiom core.cell.Cell (T : Type) : Type
 
 /- The state type used in the state-error monad -/
 axiom State : Type