From e1ee59f6a45482e93901f6a549f594fd6ef15234 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Wed, 25 Jan 2023 13:12:01 -0800
Subject: New directory structure and corresponding extraction, + misc fixes,
 for Lean

---
 tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean

(limited to 'tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean')

diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
new file mode 100644
index 00000000..87b10c59
--- /dev/null
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
@@ -0,0 +1,13 @@
+-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
+-- [hashmap_main]: opaque function definitions
+import Base.Primitives
+import HashmapMain.Types
+
+/- [hashmap_main::hashmap_utils::deserialize] -/
+axiom hashmap_utils_deserialize_fwd
+  : state -> result (state × (hashmap_hash_map_t UInt64))
+
+/- [hashmap_main::hashmap_utils::serialize] -/
+axiom hashmap_utils_serialize_fwd
+  : hashmap_hash_map_t UInt64 -> state -> result (state × Unit)
+
-- 
cgit v1.2.3