diff options
Diffstat (limited to '')
-rw-r--r-- | tests/coq/misc/External_Funs.v | 4 | ||||
-rw-r--r-- | tests/coq/misc/External_FunsExternal.v (renamed from tests/coq/misc/External_Opaque.v) | 4 | ||||
-rw-r--r-- | tests/coq/misc/External_FunsExternal_Template.v | 44 | ||||
-rw-r--r-- | tests/coq/misc/_CoqProject | 3 |
4 files changed, 50 insertions, 5 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 0a14c7d1..8a3360bb 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -8,8 +8,8 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. -Require Export External_Opaque. -Import External_Opaque. +Require Export External_FunsExternal. +Import External_FunsExternal. Module External_Funs. (** [external::swap]: forward function diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_FunsExternal.v index b482431f..07d43061 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_FunsExternal.v @@ -8,7 +8,7 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. -Module External_Opaque. +Module External_FunsExternal. (** [core::mem::swap]: forward function Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) @@ -40,4 +40,4 @@ Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . -End External_Opaque . +End External_FunsExternal. diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v new file mode 100644 index 00000000..0977c3ae --- /dev/null +++ b/tests/coq/misc/External_FunsExternal_Template.v @@ -0,0 +1,44 @@ +(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) +(** [external]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) +Require Import Primitives. +Import Primitives. +Require Import Coq.ZArith.ZArith. +Require Import List. +Import ListNotations. +Local Open Scope Primitives_scope. +Require Export External_Types. +Import External_Types. +Module External_FunsExternal_Template. + +(** [core::mem::swap]: forward function + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap : + forall(T : Type), T -> T -> state -> result (state * unit) +. + +(** [core::mem::swap]: backward function 0 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap_back0 : + forall(T : Type), T -> T -> state -> state -> result (state * T) +. + +(** [core::mem::swap]: backward function 1 + Source: '/rustc/d59363ad0b6391b7fc5bbb02c9ccf9300eef3753/library/core/src/mem/mod.rs', lines 726:0-726:42 *) +Axiom core_mem_swap_back1 : + forall(T : Type), T -> T -> state -> 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) +. + +End External_FunsExternal_Template . diff --git a/tests/coq/misc/_CoqProject b/tests/coq/misc/_CoqProject index db6c2742..6884d5d9 100644 --- a/tests/coq/misc/_CoqProject +++ b/tests/coq/misc/_CoqProject @@ -10,5 +10,6 @@ Constants.v PoloniusList.v External_Types.v NoNestedBorrows.v -External_Opaque.v +External_FunsExternal.v +External_FunsExternal_Template.v Paper.v |