diff options
Diffstat (limited to 'tests/lean/misc/external/External/Opaque.lean')
| -rw-r--r-- | tests/lean/misc/external/External/Opaque.lean | 28 | 
1 files changed, 0 insertions, 28 deletions
| diff --git a/tests/lean/misc/external/External/Opaque.lean b/tests/lean/misc/external/External/Opaque.lean deleted file mode 100644 index d3582de3..00000000 --- a/tests/lean/misc/external/External/Opaque.lean +++ /dev/null @@ -1,28 +0,0 @@ --- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS --- [external]: opaque function definitions -import Base.Primitives -import External.Types - -structure OpaqueDefs where -   -  /- [core::mem::swap] -/ -  core_mem_swap_fwd (T : Type) : T -> T -> State -> Result (State × Unit) -   -  /- [core::mem::swap] -/ -  core_mem_swap_back0 -    (T : Type) : T -> T -> State -> State -> Result (State × T) -   -  /- [core::mem::swap] -/ -  core_mem_swap_back1 -    (T : Type) : T -> T -> State -> State -> Result (State × T) -   -  /- [core::num::nonzero::NonZeroU32::{14}::new] -/ -  core_num_nonzero_non_zero_u32_new_fwd -    : -    UInt32 -> State -> Result (State × (Option -      core_num_nonzero_non_zero_u32_t)) -   -  /- [core::option::Option::{0}::unwrap] -/ -  core_option_option_unwrap_fwd -    (T : Type) : Option T -> State -> Result (State × T) -   | 
