diff options
author | Son Ho | 2023-07-05 14:52:23 +0200 |
---|---|---|
committer | Son Ho | 2023-07-05 14:52:23 +0200 |
commit | 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 (patch) | |
tree | 43fb9284e8c02ec5ed8b8a5d59f6569d66b900ff /tests/lean/External/FunsExternal_Template.lean | |
parent | 442caaf62e4a217b9a10116c4e529c49f83c4efd (diff) |
Start using namespaces in the Lean backend
Diffstat (limited to 'tests/lean/External/FunsExternal_Template.lean')
-rw-r--r-- | tests/lean/External/FunsExternal_Template.lean | 29 |
1 files changed, 29 insertions, 0 deletions
diff --git a/tests/lean/External/FunsExternal_Template.lean b/tests/lean/External/FunsExternal_Template.lean new file mode 100644 index 00000000..d6c0eb1d --- /dev/null +++ b/tests/lean/External/FunsExternal_Template.lean @@ -0,0 +1,29 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [external]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Base +import External.Types +open Primitives +open external + +/- [core::mem::swap] -/ +axiom core.mem.swap_fwd + (T : Type) : T → T → State → Result (State × Unit) + +/- [core::mem::swap] -/ +axiom core.mem.swap_back0 + (T : Type) : T → T → State → State → Result (State × T) + +/- [core::mem::swap] -/ +axiom core.mem.swap_back1 + (T : Type) : T → T → State → State → Result (State × T) + +/- [core::num::nonzero::NonZeroU32::{14}::new] -/ +axiom core.num.nonzero.NonZeroU32.new_fwd + : + U32 → State → Result (State × (Option core_num_nonzero_non_zero_u32_t)) + +/- [core::option::Option::{0}::unwrap] -/ +axiom core.option.Option.unwrap_fwd + (T : Type) : Option T → State → Result (State × T) + |