Bring order to some newlines

Came across these while rebasing.
CakeML · Oct 22, 2024 · 103027a · 103027a
1 parent 7ccfc0f
commit 103027a
Show file tree

Hide file tree

Showing 5 changed files with 1 addition and 20 deletions.
diff --git a/candle/overloading/semantics/holModelConservativityScript.sml b/candle/overloading/semantics/holModelConservativityScript.sml
@@ -2071,7 +2071,6 @@ Definition type_interpretation_ext_of0_def:
          | NONE => One (* cannot happen *)
   )
 Termination
-
   wf_rel_tac `subst_clos_term_ext_rel`
   >- (
     rw[wellorderTheory.WF_IND,subst_clos_term_ext_rel_def,WF_TC_EQN] >>
@@ -2602,7 +2601,6 @@ Termination
           fs[extends_init_def]
          )
       )
-
 End
 
 Overload type_interpretation_ext_of = ``type_interpretation_ext_of0 ^mem``

diff --git a/compiler/backend/proofs/bvi_to_dataProofScript.sml b/compiler/backend/proofs/bvi_to_dataProofScript.sml
@@ -32,6 +32,7 @@ End
 (* Projection from `dataSem$v` into `bvlSem$v` that basically gets rid of
    timestamp information (note this make the function non-injective)
 *)
+
 Definition data_to_bvi_v_def:
   data_to_bvi_v (Number i)      = bvlSem$Number i
 ∧ data_to_bvi_v (Word64 w)      = bvlSem$Word64 w

diff --git a/compiler/backend/reg_alloc/linear_scanScript.sml b/compiler/backend/reg_alloc/linear_scanScript.sml
@@ -509,10 +509,8 @@ Definition remove_inactive_intervals_def:
           return st
       )
 Termination
-
     WF_REL_TAC `measure (\(_,st). LENGTH (st.active))` >>
     rw []
-
 End
 
 Definition add_active_interval_def:
@@ -822,9 +820,7 @@ Definition partition_regs_def:
             od
         od
 Termination
-
   WF_REL_TAC `measure (\l,rpiv,begrpiv,r. r-l)`
-
 End
 
 Definition qsort_regs_def:
@@ -847,9 +843,7 @@ Definition qsort_regs_def:
             od
         od
 Termination
-
     WF_REL_TAC `measure (\l,r. r-l)`
-
 End
 
 Definition list_to_sorted_regs_def:
@@ -876,9 +870,7 @@ Definition sorted_regs_to_list_def:
           return (r::l);
         od
 Termination
-
   WF_REL_TAC `measure (\n,last. last-n)`
-
 End
 
 Definition swap_moves_def:
@@ -907,9 +899,7 @@ Definition partition_moves_def:
             od
         od
 Termination
-
   WF_REL_TAC `measure (\l,piv,r. r-l)`
-
 End
 
 Definition qsort_moves_def:
@@ -931,9 +921,7 @@ Definition qsort_moves_def:
             od
         od
 Termination
-
     WF_REL_TAC `measure (\l,r. r-l)`
-
 End
 
 
@@ -961,9 +949,7 @@ Definition sorted_moves_to_list_def:
           return (r::l);
         od
 Termination
-
   WF_REL_TAC `measure (\n,len. len-n)`
-
 End
 
 Definition linear_reg_alloc_intervals_def:

diff --git a/translator/monadic/examples/array_searchProgScript.sml b/translator/monadic/examples/array_searchProgScript.sml
@@ -75,14 +75,12 @@ Definition binary_search_aux_def:
             od
   od
 Termination
-
     WF_REL_TAC `measure (λ (_, start, finish) . finish - start)` >>
     rw[] >>
     fs[NOT_GREATER_EQ, NOT_GREATER, ADD1] >>
     `start <= (finish + start) DIV 2` by fs[X_LE_DIV]
     >- DECIDE_TAC
     >- fs[DIV_LT_X]
-
 End
 
 Definition binary_search_def:

diff --git a/translator/monadic/examples/poly_array_sortProgScript.sml b/translator/monadic/examples/poly_array_sortProgScript.sml
@@ -715,9 +715,7 @@ Definition array_get_aux_def:
       return (elem :: rest)
     od
 Termination
-
   WF_REL_TAC `measure (λ (length, n) . length - n)`
-
 End
 
 Definition array_get_def: