diff options
author | Son Ho | 2023-12-05 17:34:13 +0100 |
---|---|---|
committer | Son Ho | 2023-12-05 17:34:13 +0100 |
commit | 726db4911add81a853aafcec3936b457aaeff5b4 (patch) | |
tree | 2663915767c3558203990ed14f8d5604b7fd21d1 /tests/coq/misc/External_FunsExternal_Template.v | |
parent | 92887b89e35607e99bae2f19e4c5b2f162683d02 (diff) | |
parent | 4795e5f823bc89504855d8eb946b111d9314f4d5 (diff) |
Merge branch 'main' into son_fixes2
Diffstat (limited to 'tests/coq/misc/External_FunsExternal_Template.v')
-rw-r--r-- | tests/coq/misc/External_FunsExternal_Template.v | 44 |
1 files changed, 44 insertions, 0 deletions
diff --git a/tests/coq/misc/External_FunsExternal_Template.v b/tests/coq/misc/External_FunsExternal_Template.v new file mode 100644 index 00000000..31e69c39 --- /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 Import External_Types. +Include 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. |