diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/lean/External/Opaque.lean | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean index 1c0db095..d0297523 100644 --- a/tests/lean/External/Opaque.lean +++ b/tests/lean/External/Opaque.lean @@ -4,29 +4,29 @@ import Base import External.Types open Primitives -namespace External +namespace external structure OpaqueDefs where /- [core::mem::swap] -/ - core_mem_swap_fwd (T : Type) : T → T → State → Result (State × Unit) + core.mem.swap_fwd (T : Type) : T → T → State → Result (State × Unit) /- [core::mem::swap] -/ - core_mem_swap_back0 + core.mem.swap_back0 (T : Type) : T → T → State → State → Result (State × T) /- [core::mem::swap] -/ - core_mem_swap_back1 + 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 + core.num.nonzero.NonZeroU32.new_fwd : U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) /- [core::option::Option::{0}::unwrap] -/ - core_option_option_unwrap_fwd + core.option.Option.unwrap_fwd (T : Type) : Option T → State → Result (State × T) -end External +end external |