diff options
| author | Son HO | 2024-04-25 14:08:36 +0200 |
|---|---|---|
| committer | GitHub | 2024-04-25 14:08:36 +0200 |
| commit | a3e38d5f47e4780768902e49e28e471e38efd40a (patch) | |
| tree | 9bbce3d68895d32d2ad1118f895e7f820ef0987d /tests/lean/External/FunsExternal.lean | |
| parent | 1be37966ceea2510b911b119a96246b4657a62fd (diff) | |
| parent | e739bde5ee916af9c0c2dcf186173edba1585e4f (diff) | |
Merge pull request #135 from RaitoBezarius/option-take
compiler: add `core::option::Option::{take, is_none}` and `core::mem::swap` support
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/External/FunsExternal.lean | 23 |
1 files changed, 9 insertions, 14 deletions
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 |