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..f537fc8f --- /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]: forward function -/ +axiom hashmap_utils.deserialize + : State → Result (State × (hashmap.HashMap U64)) + +/- [hashmap_main::hashmap_utils::serialize]: forward function -/ +axiom hashmap_utils.serialize + : hashmap.HashMap U64 → State → Result (State × Unit) + |