From 703261b6c8ad680a925ae0550117a85d9dfa40fe Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 25 Apr 2024 13:42:23 +0200 Subject: Update the tests for External --- tests/coq/misc/External_FunsExternal.v | 21 +++++++-------------- 1 file changed, 7 insertions(+), 14 deletions(-) (limited to 'tests/coq/misc/External_FunsExternal.v') 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}::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. -- cgit v1.2.3