From f09eabd7c0fce7c20a0124749c841cbf5b550c52 Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Thu, 2 Feb 2023 23:49:23 -0800
Subject: All of the generated code is syntactically correct

---
 tests/lean/hashmap_on_disk/HashmapMain/Funs.lean   | 4 ++--
 tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tests/lean')

diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index ffe3416a..b0c4d683 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -5,7 +5,7 @@ import HashmapMain.Types
 import HashmapMain.Opaque
 import HashmapMain.Clauses.Template
 
-section variable (opaque_defs: OpaqueDecls)
+section variable (opaque_defs: OpaqueDefs)
 
 /- [hashmap_main::hashmap::hash_key] -/
 def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k
@@ -654,5 +654,5 @@ def insert_on_disk_fwd
 def main_fwd : result Unit := result.ret ()
 
 /- Unit test for [hashmap_main::main] -/
-#assert (main_fwd = ret ())
+#assert (main_fwd = .ret ())
 
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
index 8b41934d..ce618a6c 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Opaque.lean
@@ -3,7 +3,7 @@
 import Base.Primitives
 import HashmapMain.Types
 
-structure OpaqueDecls where
+structure OpaqueDefs where
   
   /- [hashmap_main::hashmap_utils::deserialize] -/
   hashmap_utils_deserialize_fwd
-- 
cgit v1.2.3