diff options
| author | Son HO | 2023-07-31 16:15:58 +0200 |
|---|---|---|
| committer | GitHub | 2023-07-31 16:15:58 +0200 |
| commit | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (patch) | |
| tree | 92d6021eb549f7cc25501856edd58859786b7e90 /tests/coq/misc/External_Opaque.v | |
| parent | 53adf30fe440eb8b6f58ba89f4a4c0acc7877498 (diff) | |
| parent | 9b3a58e423333fc9a4a5a264c3beb0a3d951e86b (diff) | |
Merge pull request #31 from AeneasVerif/son_lean_backend
Improve the Lean backend
Diffstat (limited to 'tests/coq/misc/External_Opaque.v')
| -rw-r--r-- | tests/coq/misc/External_Opaque.v | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v index d60251e0..1224f426 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: opaque function definitions *) +(** [external]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. @@ -8,27 +8,27 @@ Require Export External_Types. Import External_Types. Module External_Opaque. -(** [core::mem::swap] *) +(** [core::mem::swap]: forward function *) Axiom core_mem_swap_fwd : forall(T : Type), T -> T -> state -> result (state * unit) . -(** [core::mem::swap] *) +(** [core::mem::swap]: backward function 0 *) Axiom core_mem_swap_back0 : forall(T : Type), T -> T -> state -> state -> result (state * T) . -(** [core::mem::swap] *) +(** [core::mem::swap]: backward function 1 *) Axiom core_mem_swap_back1 : forall(T : Type), T -> T -> state -> state -> result (state * T) . -(** [core::num::nonzero::NonZeroU32::{14}::new] *) +(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *) Axiom core_num_nonzero_non_zero_u32_new_fwd : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t)) . -(** [core::option::Option::{0}::unwrap] *) +(** [core::option::Option::{0}::unwrap]: forward function *) Axiom core_option_option_unwrap_fwd : forall(T : Type), option T -> state -> result (state * T) . |