Make sure let-bindings in Lean end with line breaks and improve formatting

5 files changed, 36 insertions, 18 deletions

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
diff --git a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
index 2795ecfa..5b7d6f46 100644
--- a/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
+++ b/tests/lean/hashmap_on_disk/HashmapMain/Funs.lean
@@ -8,7 +8,8 @@ import HashmapMain.Clauses.Clauses
 section variable (opaque_defs: OpaqueDefs)
 
 /- [hashmap_main::hashmap::hash_key] -/
-def hashmap_hash_key_fwd (k : USize) : result USize := result.ret k
+def hashmap_hash_key_fwd (k : USize) : result USize :=
+  result.ret k
 
 /- [hashmap_main::hashmap::HashMap::{0}::allocate_slots] -/
 def hashmap_hash_map_allocate_slots_loop_fwd
@@ -638,7 +639,8 @@ def insert_on_disk_fwd
     result.ret (st1, ())
 
 /- [hashmap_main::main] -/
-def main_fwd : result Unit := result.ret ()
+def main_fwd : result Unit :=
+  result.ret ()
 
 /- Unit test for [hashmap_main::main] -/
 #assert (main_fwd = .ret ())
diff --git a/tests/lean/misc/constants/Constants.lean b/tests/lean/misc/constants/Constants.lean
index a5cbe363..9ef9ca44 100644
--- a/tests/lean/misc/constants/Constants.lean
+++ b/tests/lean/misc/constants/Constants.lean
@@ -82,7 +82,8 @@ structure OpaqueDefs where
   def y_c : wrap_t Int32 := eval_global y_body (by simp)
   
   /- [constants::unwrap_y] -/
-  def unwrap_y_fwd : result Int32 := result.ret y_c.wrap_val
+  def unwrap_y_fwd : result Int32 :=
+    result.ret y_c.wrap_val
   
   /- [constants::YVAL] -/
   def yval_body : result Int32 := unwrap_y_fwd
@@ -94,10 +95,12 @@ structure OpaqueDefs where
   def get_z1_z1_c : Int32 := eval_global get_z1_z1_body (by simp)
   
   /- [constants::get_z1] -/
-  def get_z1_fwd : result Int32 := result.ret get_z1_z1_c
+  def get_z1_fwd : result Int32 :=
+    result.ret get_z1_z1_c
   
   /- [constants::add] -/
-  def add_fwd (a : Int32) (b : Int32) : result Int32 := Int32.checked_add a b
+  def add_fwd (a : Int32) (b : Int32) : result Int32 :=
+    Int32.checked_add a b
   
   /- [constants::Q1] -/
   def q1_body : result Int32 := result.ret (Int32.ofNatCore 5 (by intlit))
diff --git a/tests/lean/misc/loops/Loops/Funs.lean b/tests/lean/misc/loops/Loops/Funs.lean
index 33a3a881..8b7e8a1f 100644
--- a/tests/lean/misc/loops/Loops/Funs.lean
+++ b/tests/lean/misc/loops/Loops/Funs.lean
@@ -221,7 +221,8 @@ def get_elem_shared_fwd
     get_elem_shared_loop_fwd x l
 
 /- [loops::id_mut] -/
-def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) := result.ret ls
+def id_mut_fwd (T : Type) (ls : list_t T) : result (list_t T) :=
+  result.ret ls
 
 /- [loops::id_mut] -/
 def id_mut_back
diff --git a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
index d871392b..53093519 100644
--- a/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
+++ b/tests/lean/misc/no_nested_borrows/NoNestedBorrows.lean
@@ -30,7 +30,8 @@ structure OpaqueDefs where
   | SumRight : T2 -> sum_t T1 T2
   
   /- [no_nested_borrows::neg_test] -/
-  def neg_test_fwd (x : Int32) : result Int32 := Int32.checked_neg x
+  def neg_test_fwd (x : Int32) : result Int32 :=
+    Int32.checked_neg x
   
   /- [no_nested_borrows::add_test] -/
   def add_test_fwd (x : UInt32) (y : UInt32) : result UInt32 :=
@@ -53,7 +54,8 @@ structure OpaqueDefs where
     UInt32.checked_rem x y
   
   /- [no_nested_borrows::cast_test] -/
-  def cast_test_fwd (x : UInt32) : result Int32 := scalar_cast Int32 x
+  def cast_test_fwd (x : UInt32) : result Int32 :=
+    scalar_cast Int32 x
   
   /- [no_nested_borrows::test2] -/
   def test2_fwd : result Unit :=
@@ -128,7 +130,8 @@ structure OpaqueDefs where
   #assert (refs_test2_fwd = .ret ())
   
   /- [no_nested_borrows::test_list1] -/
-  def test_list1_fwd : result Unit := result.ret ()
+  def test_list1_fwd : result Unit :=
+    result.ret ()
   
   /- Unit test for [no_nested_borrows::test_list1] -/
   #assert (test_list1_fwd = .ret ())
@@ -145,7 +148,8 @@ structure OpaqueDefs where
   #assert (test_box1_fwd = .ret ())
   
   /- [no_nested_borrows::copy_int] -/
-  def copy_int_fwd (x : Int32) : result Int32 := result.ret x
+  def copy_int_fwd (x : Int32) : result Int32 :=
+    result.ret x
   
   /- [no_nested_borrows::test_unreachable] -/
   def test_unreachable_fwd (b : Bool) : result Unit :=
@@ -240,7 +244,8 @@ structure OpaqueDefs where
   #assert (choose_test_fwd = .ret ())
   
   /- [no_nested_borrows::test_char] -/
-  def test_char_fwd : result Char := result.ret 'a'
+  def test_char_fwd : result Char :=
+    result.ret 'a'
   
   /- [no_nested_borrows::NodeElem] -/
   mutual inductive node_elem_t (T : Type) :=
@@ -389,16 +394,19 @@ structure OpaqueDefs where
   /- [no_nested_borrows::id_mut_pair1] -/
   def id_mut_pair1_back
     (T1 T2 : Type) (x : T1) (y : T2) (ret0 : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := ret0 result.ret (t, t0)
+    let (t, t0) := ret0
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair2] -/
   def id_mut_pair2_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := p result.ret (t, t0)
+    let (t, t0) := p
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair2] -/
   def id_mut_pair2_back
     (T1 T2 : Type) (p : (T1 × T2)) (ret0 : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := ret0 result.ret (t, t0)
+    let (t, t0) := ret0
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair3] -/
   def id_mut_pair3_fwd (T1 T2 : Type) (x : T1) (y : T2) : result (T1 × T2) :=
@@ -416,7 +424,8 @@ structure OpaqueDefs where
   
   /- [no_nested_borrows::id_mut_pair4] -/
   def id_mut_pair4_fwd (T1 T2 : Type) (p : (T1 × T2)) : result (T1 × T2) :=
-    let (t, t0) := p result.ret (t, t0)
+    let (t, t0) := p
+    result.ret (t, t0)
   
   /- [no_nested_borrows::id_mut_pair4] -/
   def id_mut_pair4_back'a
@@ -505,7 +514,8 @@ structure OpaqueDefs where
   #assert (test_constants_fwd = .ret ())
   
   /- [no_nested_borrows::test_weird_borrows1] -/
-  def test_weird_borrows1_fwd : result Unit := result.ret ()
+  def test_weird_borrows1_fwd : result Unit :=
+    result.ret ()
   
   /- Unit test for [no_nested_borrows::test_weird_borrows1] -/
   #assert (test_weird_borrows1_fwd = .ret ())