summaryrefslogtreecommitdiff
path: root/tests/lean/misc/external/External/Opaque.lean
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/misc/external/External/Opaque.lean')
-rw-r--r--tests/lean/misc/external/External/Opaque.lean28
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)
-