diff options
author | Son Ho | 2023-07-04 18:09:36 +0200 |
---|---|---|
committer | Son Ho | 2023-07-04 18:09:36 +0200 |
commit | b643bd00747e75d69b6066c55a1798b61277c4b6 (patch) | |
tree | 84bbebe82964efc0d779ea782f3ae4b946ca3483 /tests/lean/External/Opaque.lean | |
parent | 74b3ce71b0e3794853aa1413afaaaa05c8cc5a84 (diff) |
Regenerate the Lean test files
Diffstat (limited to '')
-rw-r--r-- | tests/lean/External/Opaque.lean | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/tests/lean/External/Opaque.lean b/tests/lean/External/Opaque.lean index 5483c3a9..1c0db095 100644 --- a/tests/lean/External/Opaque.lean +++ b/tests/lean/External/Opaque.lean @@ -4,25 +4,29 @@ import Base import External.Types open Primitives +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 - (T : Type) : T -> T -> State -> State -> Result (State × T) + (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) + (T : Type) : T → T → State → State → Result (State × T) /- [core::num::nonzero::NonZeroU32::{14}::new] -/ core_num_nonzero_non_zero_u32_new_fwd : - U32 -> State -> Result (State × (Option core_num_nonzero_non_zero_u32_t)) + U32 → 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) + (T : Type) : Option T → State → Result (State × T) +end External |