summaryrefslogtreecommitdiff
path: root/tests/lean/External/FunsExternal.lean
diff options
context:
space:
mode:
authorSon Ho2024-04-25 16:07:56 +0200
committerSon Ho2024-04-25 16:07:56 +0200
commit078b7f59ddfcb12a7b4c69f0a51bfd57cb391ddf (patch)
treeed45664329e24d1773be6c8bcaf827e2adbd3f65 /tests/lean/External/FunsExternal.lean
parent1728dced8484befe35ef61fdf4ccd62b93fbb19d (diff)
parenta3e38d5f47e4780768902e49e28e471e38efd40a (diff)
Merge branch 'main' into core-option-unwrap
Diffstat (limited to '')
-rw-r--r--tests/lean/External/FunsExternal.lean19
1 files changed, 9 insertions, 10 deletions
diff --git a/tests/lean/External/FunsExternal.lean b/tests/lean/External/FunsExternal.lean
index 7adf0922..c3e8dd79 100644
--- a/tests/lean/External/FunsExternal.lean
+++ b/tests/lean/External/FunsExternal.lean
@@ -4,14 +4,13 @@ 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::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::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