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/coq/misc/External_FunsExternal.v | |
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 'tests/coq/misc/External_FunsExternal.v')
-rw-r--r-- | tests/coq/misc/External_FunsExternal.v | 21 |
1 files changed, 7 insertions, 14 deletions
diff --git a/tests/coq/misc/External_FunsExternal.v b/tests/coq/misc/External_FunsExternal.v index 39f4a60e..a25d9c33 100644 --- a/tests/coq/misc/External_FunsExternal.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -9,22 +9,15 @@ Require Export External_Types. Include External_Types. Module External_FunsExternal. -(** [core::mem::swap]: - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) -Definition core_mem_swap (T : Type) (x : T) (y : T) (s : state) := - Ok (s, (y, x)) +Axiom core_cell_Cell_get : + forall(T : Type) (markerCopyInst : core_marker_Copy_t T), + core_cell_Cell_t T -> state -> result (state * T) . -(** [core::num::nonzero::{core::num::nonzero::NonZeroU32#14}::new]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/num/nonzero.rs', lines 79:16-79:57 *) -Axiom core_num_nonzero_NonZeroU32_new - : u32 -> state -> result (state * (option core_num_nonzero_NonZeroU32_t)) -. - -(** [core::option::{core::option::Option<T>}::unwrap]: forward function - Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/option.rs', lines 932:4-932:34 *) -Axiom core_option_Option_unwrap : - forall(T : Type), option T -> state -> result (state * T) +Axiom core_cell_Cell_get_mut : + forall(T : Type), + core_cell_Cell_t T -> state -> result (state * (T * (T -> state -> + result (state * (core_cell_Cell_t T))))) . End External_FunsExternal. |