diff options
Diffstat (limited to 'tests/lean/HashmapMain/FunsExternal_Template.lean')
| -rw-r--r-- | tests/lean/HashmapMain/FunsExternal_Template.lean | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/tests/lean/HashmapMain/FunsExternal_Template.lean b/tests/lean/HashmapMain/FunsExternal_Template.lean new file mode 100644 index 00000000..86286373 --- /dev/null +++ b/tests/lean/HashmapMain/FunsExternal_Template.lean @@ -0,0 +1,16 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [hashmap_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. +import Base +import HashmapMain.Types +open Primitives +open hashmap_main + +/- [hashmap_main::hashmap_utils::deserialize] -/ +axiom hashmap_utils.deserialize_fwd + : State → Result (State × (hashmap_hash_map_t U64)) + +/- [hashmap_main::hashmap_utils::serialize] -/ +axiom hashmap_utils.serialize_fwd + : hashmap_hash_map_t U64 → State → Result (State × Unit) + |