diff options
Diffstat (limited to 'tests/lean/External/FunsExternal.lean')
-rw-r--r-- | tests/lean/External/FunsExternal.lean | 19 |
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 |