From c6913b8bf90689d8961c47f59896443e7fae164d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sun, 5 Feb 2023 22:03:41 +0100
Subject: Make sure let-bindings in Lean end with line breaks and improve
 formatting

---
 tests/lean/hashmap/Hashmap/Funs.lean | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'tests/lean/hashmap/Hashmap')

diff --git a/tests/lean/hashmap/Hashmap/Funs.lean b/tests/lean/hashmap/Hashmap/Funs.lean
index 1b03b7a2..78ed970a 100644
--- a/tests/lean/hashmap/Hashmap/Funs.lean
+++ b/tests/lean/hashmap/Hashmap/Funs.lean
@@ -5,7 +5,8 @@ import Hashmap.Types
 import Hashmap.Clauses.Clauses
 
 /- [hashmap::hash_key] -/
-def hash_key_fwd (k : USize) : result USize := result.ret k
+def hash_key_fwd (k : USize) : result USize :=
+  result.ret k
 
 /- [hashmap::HashMap::{0}::allocate_slots] -/
 def hash_map_allocate_slots_loop_fwd
@@ -119,7 +120,8 @@ def hash_map_insert_in_list_loop_back
         let tl0 <- hash_map_insert_in_list_loop_back T key value tl
         result.ret (list_t.ListCons ckey cvalue tl0)
   | list_t.ListNil =>
-    let l := list_t.ListNil result.ret (list_t.ListCons key value l)
+    let l := list_t.ListNil
+    result.ret (list_t.ListCons key value l)
   
 termination_by hash_map_insert_in_list_loop_back key value ls =>
   hash_map_insert_in_list_loop_terminates T key value ls
-- 
cgit v1.2.3