Rename some subdirectories for consistency

5 files changed, 0 insertions, 1598 deletions

diff --git a/tests/hol4/misc-loops/Holmakefile b/tests/hol4/misc-loops/Holmakefile
deleted file mode 100644
index 3c4b8973..00000000
--- a/tests/hol4/misc-loops/Holmakefile
+++ /dev/null
@@ -1,5 +0,0 @@
-# This file was automatically generated - modify ../Holmakefile.template instead
-INCLUDES =  ../../../backends/hol4
-
-all: $(DEFAULT_TARGETS)
-.PHONY: all
diff --git a/tests/hol4/misc-loops/loops_FunsScript.sml b/tests/hol4/misc-loops/loops_FunsScript.sml
deleted file mode 100644
index 65cf77d4..00000000
--- a/tests/hol4/misc-loops/loops_FunsScript.sml
+++ /dev/null
@@ -1,755 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [loops]: function definitions *)
-open primitivesLib divDefLib
-open loops_TypesTheory
-
-val _ = new_theory "loops_Funs"
-
-
-val [sum_loop_fwd_def] = DefineDiv ‘
-  (** [loops::sum]: loop 0: forward function *)
-  sum_loop_fwd (max : u32) (i : u32) (s : u32) : u32 result =
-    if u32_lt i max
-    then (
-      do
-      s0 <- u32_add s i;
-      i0 <- u32_add i (int_to_u32 1);
-      sum_loop_fwd max i0 s0
-      od)
-    else u32_mul s (int_to_u32 2)
-’
-
-val sum_fwd_def = Define ‘
-  (** [loops::sum]: forward function *)
-  sum_fwd (max : u32) : u32 result =
-    sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [sum_with_mut_borrows_loop_fwd_def] = DefineDiv ‘
-  (** [loops::sum_with_mut_borrows]: loop 0: forward function *)
-  sum_with_mut_borrows_loop_fwd
-    (max : u32) (mi : u32) (ms : u32) : u32 result =
-    if u32_lt mi max
-    then (
-      do
-      ms0 <- u32_add ms mi;
-      mi0 <- u32_add mi (int_to_u32 1);
-      sum_with_mut_borrows_loop_fwd max mi0 ms0
-      od)
-    else u32_mul ms (int_to_u32 2)
-’
-
-val sum_with_mut_borrows_fwd_def = Define ‘
-  (** [loops::sum_with_mut_borrows]: forward function *)
-  sum_with_mut_borrows_fwd (max : u32) : u32 result =
-    sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [sum_with_shared_borrows_loop_fwd_def] = DefineDiv ‘
-  (** [loops::sum_with_shared_borrows]: loop 0: forward function *)
-  sum_with_shared_borrows_loop_fwd
-    (max : u32) (i : u32) (s : u32) : u32 result =
-    if u32_lt i max
-    then (
-      do
-      i0 <- u32_add i (int_to_u32 1);
-      s0 <- u32_add s i0;
-      sum_with_shared_borrows_loop_fwd max i0 s0
-      od)
-    else u32_mul s (int_to_u32 2)
-’
-
-val sum_with_shared_borrows_fwd_def = Define ‘
-  (** [loops::sum_with_shared_borrows]: forward function *)
-  sum_with_shared_borrows_fwd (max : u32) : u32 result =
-    sum_with_shared_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-’
-
-val [clear_loop_fwd_back_def] = DefineDiv ‘
-  (** [loops::clear]: loop 0: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  clear_loop_fwd_back (v : u32 vec) (i : usize) : u32 vec result =
-    let i0 = vec_len v in
-    if usize_lt i i0
-    then (
-      do
-      i1 <- usize_add i (int_to_usize 1);
-      v0 <- vec_index_mut_back v i (int_to_u32 0);
-      clear_loop_fwd_back v0 i1
-      od)
-    else Return v
-’
-
-val clear_fwd_back_def = Define ‘
-  (** [loops::clear]: merged forward/backward function
-      (there is a single backward function, and the forward function returns ()) *)
-  clear_fwd_back (v : u32 vec) : u32 vec result =
-    clear_loop_fwd_back v (int_to_usize 0)
-’
-
-val [list_mem_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_mem]: loop 0: forward function *)
-  list_mem_loop_fwd (x : u32) (ls : u32 list_t) : bool result =
-    (case ls of
-    | ListCons y tl => if y = x then Return T else list_mem_loop_fwd x tl
-    | ListNil => Return F)
-’
-
-val list_mem_fwd_def = Define ‘
-  (** [loops::list_mem]: forward function *)
-  list_mem_fwd (x : u32) (ls : u32 list_t) : bool result =
-    list_mem_loop_fwd x ls
-’
-
-val [list_nth_mut_loop_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop]: loop 0: forward function *)
-  list_nth_mut_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return x
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        list_nth_mut_loop_loop_fwd tl i0
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_fwd_def = Define ‘
-  (** [loops::list_nth_mut_loop]: forward function *)
-  list_nth_mut_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-    list_nth_mut_loop_loop_fwd ls i
-’
-
-val [list_nth_mut_loop_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop]: loop 0: backward function 0 *)
-  list_nth_mut_loop_loop_back
-    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return (ListCons ret tl)
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
-        Return (ListCons x tl0)
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_back_def = Define ‘
-  (** [loops::list_nth_mut_loop]: backward function 0 *)
-  list_nth_mut_loop_back
-    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
-    list_nth_mut_loop_loop_back ls i ret
-’
-
-val [list_nth_shared_loop_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_loop]: loop 0: forward function *)
-  list_nth_shared_loop_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return x
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        list_nth_shared_loop_loop_fwd tl i0
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_fwd_def = Define ‘
-  (** [loops::list_nth_shared_loop]: forward function *)
-  list_nth_shared_loop_fwd (ls : 't list_t) (i : u32) : 't result =
-    list_nth_shared_loop_loop_fwd ls i
-’
-
-val [get_elem_mut_loop_fwd_def] = DefineDiv ‘
-  (** [loops::get_elem_mut]: loop 0: forward function *)
-  get_elem_mut_loop_fwd (x : usize) (ls : usize list_t) : usize result =
-    (case ls of
-    | ListCons y tl => if y = x then Return y else get_elem_mut_loop_fwd x tl
-    | ListNil => Fail Failure)
-’
-
-val get_elem_mut_fwd_def = Define ‘
-  (** [loops::get_elem_mut]: forward function *)
-  get_elem_mut_fwd (slots : usize list_t vec) (x : usize) : usize result =
-    do
-    l <- vec_index_mut_fwd slots (int_to_usize 0);
-    get_elem_mut_loop_fwd x l
-    od
-’
-
-val [get_elem_mut_loop_back_def] = DefineDiv ‘
-  (** [loops::get_elem_mut]: loop 0: backward function 0 *)
-  get_elem_mut_loop_back
-    (x : usize) (ls : usize list_t) (ret : usize) : usize list_t result =
-    (case ls of
-    | ListCons y tl =>
-      if y = x
-      then Return (ListCons ret tl)
-      else (
-        do
-        tl0 <- get_elem_mut_loop_back x tl ret;
-        Return (ListCons y tl0)
-        od)
-    | ListNil => Fail Failure)
-’
-
-val get_elem_mut_back_def = Define ‘
-  (** [loops::get_elem_mut]: backward function 0 *)
-  get_elem_mut_back
-    (slots : usize list_t vec) (x : usize) (ret : usize) :
-    usize list_t vec result
-    =
-    do
-    l <- vec_index_mut_fwd slots (int_to_usize 0);
-    l0 <- get_elem_mut_loop_back x l ret;
-    vec_index_mut_back slots (int_to_usize 0) l0
-    od
-’
-
-val [get_elem_shared_loop_fwd_def] = DefineDiv ‘
-  (** [loops::get_elem_shared]: loop 0: forward function *)
-  get_elem_shared_loop_fwd (x : usize) (ls : usize list_t) : usize result =
-    (case ls of
-    | ListCons y tl =>
-      if y = x then Return y else get_elem_shared_loop_fwd x tl
-    | ListNil => Fail Failure)
-’
-
-val get_elem_shared_fwd_def = Define ‘
-  (** [loops::get_elem_shared]: forward function *)
-  get_elem_shared_fwd (slots : usize list_t vec) (x : usize) : usize result =
-    do
-    l <- vec_index_fwd slots (int_to_usize 0);
-    get_elem_shared_loop_fwd x l
-    od
-’
-
-val id_mut_fwd_def = Define ‘
-  (** [loops::id_mut]: forward function *)
-  id_mut_fwd (ls : 't list_t) : 't list_t result =
-    Return ls
-’
-
-val id_mut_back_def = Define ‘
-  (** [loops::id_mut]: backward function 0 *)
-  id_mut_back (ls : 't list_t) (ret : 't list_t) : 't list_t result =
-    Return ret
-’
-
-val id_shared_fwd_def = Define ‘
-  (** [loops::id_shared]: forward function *)
-  id_shared_fwd (ls : 't list_t) : 't list_t result =
-    Return ls
-’
-
-val [list_nth_mut_loop_with_id_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_with_id]: loop 0: forward function *)
-  list_nth_mut_loop_with_id_loop_fwd (i : u32) (ls : 't list_t) : 't result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return x
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        list_nth_mut_loop_with_id_loop_fwd i0 tl
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_with_id_fwd_def = Define ‘
-  (** [loops::list_nth_mut_loop_with_id]: forward function *)
-  list_nth_mut_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
-    do
-    ls0 <- id_mut_fwd ls;
-    list_nth_mut_loop_with_id_loop_fwd i ls0
-    od
-’
-
-val [list_nth_mut_loop_with_id_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_with_id]: loop 0: backward function 0 *)
-  list_nth_mut_loop_with_id_loop_back
-    (i : u32) (ls : 't list_t) (ret : 't) : 't list_t result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return (ListCons ret tl)
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
-        Return (ListCons x tl0)
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_with_id_back_def = Define ‘
-  (** [loops::list_nth_mut_loop_with_id]: backward function 0 *)
-  list_nth_mut_loop_with_id_back
-    (ls : 't list_t) (i : u32) (ret : 't) : 't list_t result =
-    do
-    ls0 <- id_mut_fwd ls;
-    l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
-    id_mut_back ls l
-    od
-’
-
-val [list_nth_shared_loop_with_id_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_loop_with_id]: loop 0: forward function *)
-  list_nth_shared_loop_with_id_loop_fwd
-    (i : u32) (ls : 't list_t) : 't result =
-    (case ls of
-    | ListCons x tl =>
-      if i = int_to_u32 0
-      then Return x
-      else (
-        do
-        i0 <- u32_sub i (int_to_u32 1);
-        list_nth_shared_loop_with_id_loop_fwd i0 tl
-        od)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_with_id_fwd_def = Define ‘
-  (** [loops::list_nth_shared_loop_with_id]: forward function *)
-  list_nth_shared_loop_with_id_fwd (ls : 't list_t) (i : u32) : 't result =
-    do
-    ls0 <- id_shared_fwd ls;
-    list_nth_shared_loop_with_id_loop_fwd i ls0
-    od
-’
-
-val [list_nth_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_pair]: loop 0: forward function *)
-  list_nth_mut_loop_pair_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_fwd_def = Define ‘
-  (** [loops::list_nth_mut_loop_pair]: forward function *)
-  list_nth_mut_loop_pair_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_loop_back'a_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 0 *)
-  list_nth_mut_loop_pair_loop_back'a
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl0)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl00 <- list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_back'a_def = Define ‘
-  (** [loops::list_nth_mut_loop_pair]: backward function 0 *)
-  list_nth_mut_loop_pair_back'a
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
-’
-
-val [list_nth_mut_loop_pair_loop_back'b_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_pair]: loop 0: backward function 1 *)
-  list_nth_mut_loop_pair_loop_back'b
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl10 <- list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_back'b_def = Define ‘
-  (** [loops::list_nth_mut_loop_pair]: backward function 1 *)
-  list_nth_mut_loop_pair_back'b
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
-’
-
-val [list_nth_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_loop_pair]: loop 0: forward function *)
-  list_nth_shared_loop_pair_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_pair_fwd_def = Define ‘
-  (** [loops::list_nth_shared_loop_pair]: forward function *)
-  list_nth_shared_loop_pair_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_pair_merge]: loop 0: forward function *)
-  list_nth_mut_loop_pair_merge_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_merge_fwd_def = Define ‘
-  (** [loops::list_nth_mut_loop_pair_merge]: forward function *)
-  list_nth_mut_loop_pair_merge_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_loop_pair_merge]: loop 0: backward function 0 *)
-  list_nth_mut_loop_pair_merge_loop_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
-    ('t list_t # 't list_t) result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then let (t, t0) = ret in Return (ListCons t tl0, ListCons t0 tl1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          (tl00, tl10) <-
-            list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00, ListCons x1 tl10)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_loop_pair_merge_back_def = Define ‘
-  (** [loops::list_nth_mut_loop_pair_merge]: backward function 0 *)
-  list_nth_mut_loop_pair_merge_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : ('t # 't)) :
-    ('t list_t # 't list_t) result
-    =
-    list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_loop_pair_merge]: loop 0: forward function *)
-  list_nth_shared_loop_pair_merge_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_loop_pair_merge_fwd_def = Define ‘
-  (** [loops::list_nth_shared_loop_pair_merge]: forward function *)
-  list_nth_shared_loop_pair_merge_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_shared_loop_pair]: loop 0: forward function *)
-  list_nth_mut_shared_loop_pair_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_fwd_def = Define ‘
-  (** [loops::list_nth_mut_shared_loop_pair]: forward function *)
-  list_nth_mut_shared_loop_pair_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_shared_loop_pair]: loop 0: backward function 0 *)
-  list_nth_mut_shared_loop_pair_loop_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl0)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl00 <- list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_back_def = Define ‘
-  (** [loops::list_nth_mut_shared_loop_pair]: backward function 0 *)
-  list_nth_mut_shared_loop_pair_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_mut_shared_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: forward function *)
-  list_nth_mut_shared_loop_pair_merge_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_merge_fwd_def = Define ‘
-  (** [loops::list_nth_mut_shared_loop_pair_merge]: forward function *)
-  list_nth_mut_shared_loop_pair_merge_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_mut_shared_loop_pair_merge_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_mut_shared_loop_pair_merge]: loop 0: backward function 0 *)
-  list_nth_mut_shared_loop_pair_merge_loop_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl0)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl00 <- list_nth_mut_shared_loop_pair_merge_loop_back tl0 tl1 i0 ret;
-          Return (ListCons x0 tl00)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_mut_shared_loop_pair_merge_back_def = Define ‘
-  (** [loops::list_nth_mut_shared_loop_pair_merge]: backward function 0 *)
-  list_nth_mut_shared_loop_pair_merge_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_mut_loop_pair_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_mut_loop_pair]: loop 0: forward function *)
-  list_nth_shared_mut_loop_pair_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_fwd_def = Define ‘
-  (** [loops::list_nth_shared_mut_loop_pair]: forward function *)
-  list_nth_shared_mut_loop_pair_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_shared_mut_loop_pair_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_mut_loop_pair]: loop 0: backward function 1 *)
-  list_nth_shared_mut_loop_pair_loop_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl10 <- list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_back_def = Define ‘
-  (** [loops::list_nth_shared_mut_loop_pair]: backward function 1 *)
-  list_nth_shared_mut_loop_pair_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
-’
-
-val [list_nth_shared_mut_loop_pair_merge_loop_fwd_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: forward function *)
-  list_nth_shared_mut_loop_pair_merge_loop_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (x0, x1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_merge_fwd_def = Define ‘
-  (** [loops::list_nth_shared_mut_loop_pair_merge]: forward function *)
-  list_nth_shared_mut_loop_pair_merge_fwd
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) : ('t # 't) result =
-    list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-’
-
-val [list_nth_shared_mut_loop_pair_merge_loop_back_def] = DefineDiv ‘
-  (** [loops::list_nth_shared_mut_loop_pair_merge]: loop 0: backward function 0 *)
-  list_nth_shared_mut_loop_pair_merge_loop_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    (case ls0 of
-    | ListCons x0 tl0 =>
-      (case ls1 of
-      | ListCons x1 tl1 =>
-        if i = int_to_u32 0
-        then Return (ListCons ret tl1)
-        else (
-          do
-          i0 <- u32_sub i (int_to_u32 1);
-          tl10 <- list_nth_shared_mut_loop_pair_merge_loop_back tl0 tl1 i0 ret;
-          Return (ListCons x1 tl10)
-          od)
-      | ListNil => Fail Failure)
-    | ListNil => Fail Failure)
-’
-
-val list_nth_shared_mut_loop_pair_merge_back_def = Define ‘
-  (** [loops::list_nth_shared_mut_loop_pair_merge]: backward function 0 *)
-  list_nth_shared_mut_loop_pair_merge_back
-    (ls0 : 't list_t) (ls1 : 't list_t) (i : u32) (ret : 't) :
-    't list_t result
-    =
-    list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-’
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-loops/loops_FunsTheory.sig b/tests/hol4/misc-loops/loops_FunsTheory.sig
deleted file mode 100644
index 63fe56c9..00000000
--- a/tests/hol4/misc-loops/loops_FunsTheory.sig
+++ /dev/null
@@ -1,731 +0,0 @@
-signature loops_FunsTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val clear_fwd_back_def : thm
-    val clear_loop_fwd_back_def : thm
-    val get_elem_mut_back_def : thm
-    val get_elem_mut_fwd_def : thm
-    val get_elem_mut_loop_back_def : thm
-    val get_elem_mut_loop_fwd_def : thm
-    val get_elem_shared_fwd_def : thm
-    val get_elem_shared_loop_fwd_def : thm
-    val id_mut_back_def : thm
-    val id_mut_fwd_def : thm
-    val id_shared_fwd_def : thm
-    val list_mem_fwd_def : thm
-    val list_mem_loop_fwd_def : thm
-    val list_nth_mut_loop_back_def : thm
-    val list_nth_mut_loop_fwd_def : thm
-    val list_nth_mut_loop_loop_back_def : thm
-    val list_nth_mut_loop_loop_fwd_def : thm
-    val list_nth_mut_loop_pair_back'a_def : thm
-    val list_nth_mut_loop_pair_back'b_def : thm
-    val list_nth_mut_loop_pair_fwd_def : thm
-    val list_nth_mut_loop_pair_loop_back'a_def : thm
-    val list_nth_mut_loop_pair_loop_back'b_def : thm
-    val list_nth_mut_loop_pair_loop_fwd_def : thm
-    val list_nth_mut_loop_pair_merge_back_def : thm
-    val list_nth_mut_loop_pair_merge_fwd_def : thm
-    val list_nth_mut_loop_pair_merge_loop_back_def : thm
-    val list_nth_mut_loop_pair_merge_loop_fwd_def : thm
-    val list_nth_mut_loop_with_id_back_def : thm
-    val list_nth_mut_loop_with_id_fwd_def : thm
-    val list_nth_mut_loop_with_id_loop_back_def : thm
-    val list_nth_mut_loop_with_id_loop_fwd_def : thm
-    val list_nth_mut_shared_loop_pair_back_def : thm
-    val list_nth_mut_shared_loop_pair_fwd_def : thm
-    val list_nth_mut_shared_loop_pair_loop_back_def : thm
-    val list_nth_mut_shared_loop_pair_loop_fwd_def : thm
-    val list_nth_mut_shared_loop_pair_merge_back_def : thm
-    val list_nth_mut_shared_loop_pair_merge_fwd_def : thm
-    val list_nth_mut_shared_loop_pair_merge_loop_back_def : thm
-    val list_nth_mut_shared_loop_pair_merge_loop_fwd_def : thm
-    val list_nth_shared_loop_fwd_def : thm
-    val list_nth_shared_loop_loop_fwd_def : thm
-    val list_nth_shared_loop_pair_fwd_def : thm
-    val list_nth_shared_loop_pair_loop_fwd_def : thm
-    val list_nth_shared_loop_pair_merge_fwd_def : thm
-    val list_nth_shared_loop_pair_merge_loop_fwd_def : thm
-    val list_nth_shared_loop_with_id_fwd_def : thm
-    val list_nth_shared_loop_with_id_loop_fwd_def : thm
-    val list_nth_shared_mut_loop_pair_back_def : thm
-    val list_nth_shared_mut_loop_pair_fwd_def : thm
-    val list_nth_shared_mut_loop_pair_loop_back_def : thm
-    val list_nth_shared_mut_loop_pair_loop_fwd_def : thm
-    val list_nth_shared_mut_loop_pair_merge_back_def : thm
-    val list_nth_shared_mut_loop_pair_merge_fwd_def : thm
-    val list_nth_shared_mut_loop_pair_merge_loop_back_def : thm
-    val list_nth_shared_mut_loop_pair_merge_loop_fwd_def : thm
-    val sum_fwd_def : thm
-    val sum_loop_fwd_def : thm
-    val sum_with_mut_borrows_fwd_def : thm
-    val sum_with_mut_borrows_loop_fwd_def : thm
-    val sum_with_shared_borrows_fwd_def : thm
-    val sum_with_shared_borrows_loop_fwd_def : thm
-  
-  val loops_Funs_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [loops_Types] Parent theory of "loops_Funs"
-   
-   [clear_fwd_back_def]  Definition
-      
-      ⊢ ∀v. clear_fwd_back v = clear_loop_fwd_back v (int_to_usize 0)
-   
-   [clear_loop_fwd_back_def]  Definition
-      
-      ⊢ ∀v i.
-          clear_loop_fwd_back v i =
-          (let
-             i0 = vec_len v
-           in
-             if usize_lt i i0 then
-               do
-                 i1 <- usize_add i (int_to_usize 1);
-                 v0 <- vec_index_mut_back v i (int_to_u32 0);
-                 clear_loop_fwd_back v0 i1
-               od
-             else Return v)
-   
-   [get_elem_mut_back_def]  Definition
-      
-      ⊢ ∀slots x ret.
-          get_elem_mut_back slots x ret =
-          do
-            l <- vec_index_mut_fwd slots (int_to_usize 0);
-            l0 <- get_elem_mut_loop_back x l ret;
-            vec_index_mut_back slots (int_to_usize 0) l0
-          od
-   
-   [get_elem_mut_fwd_def]  Definition
-      
-      ⊢ ∀slots x.
-          get_elem_mut_fwd slots x =
-          do
-            l <- vec_index_mut_fwd slots (int_to_usize 0);
-            get_elem_mut_loop_fwd x l
-          od
-   
-   [get_elem_mut_loop_back_def]  Definition
-      
-      ⊢ ∀x ls ret.
-          get_elem_mut_loop_back x ls ret =
-          case ls of
-            ListCons y tl =>
-              if y = x then Return (ListCons ret tl)
-              else
-                do
-                  tl0 <- get_elem_mut_loop_back x tl ret;
-                  Return (ListCons y tl0)
-                od
-          | ListNil => Fail Failure
-   
-   [get_elem_mut_loop_fwd_def]  Definition
-      
-      ⊢ ∀x ls.
-          get_elem_mut_loop_fwd x ls =
-          case ls of
-            ListCons y tl =>
-              if y = x then Return y else get_elem_mut_loop_fwd x tl
-          | ListNil => Fail Failure
-   
-   [get_elem_shared_fwd_def]  Definition
-      
-      ⊢ ∀slots x.
-          get_elem_shared_fwd slots x =
-          do
-            l <- vec_index_fwd slots (int_to_usize 0);
-            get_elem_shared_loop_fwd x l
-          od
-   
-   [get_elem_shared_loop_fwd_def]  Definition
-      
-      ⊢ ∀x ls.
-          get_elem_shared_loop_fwd x ls =
-          case ls of
-            ListCons y tl =>
-              if y = x then Return y else get_elem_shared_loop_fwd x tl
-          | ListNil => Fail Failure
-   
-   [id_mut_back_def]  Definition
-      
-      ⊢ ∀ls ret. id_mut_back ls ret = Return ret
-   
-   [id_mut_fwd_def]  Definition
-      
-      ⊢ ∀ls. id_mut_fwd ls = Return ls
-   
-   [id_shared_fwd_def]  Definition
-      
-      ⊢ ∀ls. id_shared_fwd ls = Return ls
-   
-   [list_mem_fwd_def]  Definition
-      
-      ⊢ ∀x ls. list_mem_fwd x ls = list_mem_loop_fwd x ls
-   
-   [list_mem_loop_fwd_def]  Definition
-      
-      ⊢ ∀x ls.
-          list_mem_loop_fwd x ls =
-          case ls of
-            ListCons y tl =>
-              if y = x then Return T else list_mem_loop_fwd x tl
-          | ListNil => Return F
-   
-   [list_nth_mut_loop_back_def]  Definition
-      
-      ⊢ ∀ls i ret.
-          list_nth_mut_loop_back ls i ret =
-          list_nth_mut_loop_loop_back ls i ret
-   
-   [list_nth_mut_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls i. list_nth_mut_loop_fwd ls i = list_nth_mut_loop_loop_fwd ls i
-   
-   [list_nth_mut_loop_loop_back_def]  Definition
-      
-      ⊢ ∀ls i ret.
-          list_nth_mut_loop_loop_back ls i ret =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return (ListCons ret tl)
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  tl0 <- list_nth_mut_loop_loop_back tl i0 ret;
-                  Return (ListCons x tl0)
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls i.
-          list_nth_mut_loop_loop_fwd ls i =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return x
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  list_nth_mut_loop_loop_fwd tl i0
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_pair_back'a_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_back'a ls0 ls1 i ret =
-          list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret
-   
-   [list_nth_mut_loop_pair_back'b_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_back'b ls0 ls1 i ret =
-          list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret
-   
-   [list_nth_mut_loop_pair_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_loop_pair_fwd ls0 ls1 i =
-          list_nth_mut_loop_pair_loop_fwd ls0 ls1 i
-   
-   [list_nth_mut_loop_pair_loop_back'a_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_loop_back'a ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl0)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl00 <-
-                         list_nth_mut_loop_pair_loop_back'a tl0 tl1 i0 ret;
-                       Return (ListCons x0 tl00)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_pair_loop_back'b_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_loop_back'b ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl10 <-
-                         list_nth_mut_loop_pair_loop_back'b tl0 tl1 i0 ret;
-                       Return (ListCons x1 tl10)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_pair_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_loop_pair_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_mut_loop_pair_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_pair_merge_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_merge_back ls0 ls1 i ret =
-          list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-   
-   [list_nth_mut_loop_pair_merge_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_loop_pair_merge_fwd ls0 ls1 i =
-          list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-   
-   [list_nth_mut_loop_pair_merge_loop_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then
-                     (let
-                        (t,t0) = ret
-                      in
-                        Return (ListCons t tl0,ListCons t0 tl1))
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       (tl00,tl10) <-
-                         list_nth_mut_loop_pair_merge_loop_back tl0 tl1 i0
-                           ret;
-                       Return (ListCons x0 tl00,ListCons x1 tl10)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_pair_merge_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_mut_loop_pair_merge_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_with_id_back_def]  Definition
-      
-      ⊢ ∀ls i ret.
-          list_nth_mut_loop_with_id_back ls i ret =
-          do
-            ls0 <- id_mut_fwd ls;
-            l <- list_nth_mut_loop_with_id_loop_back i ls0 ret;
-            id_mut_back ls l
-          od
-   
-   [list_nth_mut_loop_with_id_fwd_def]  Definition
-      
-      ⊢ ∀ls i.
-          list_nth_mut_loop_with_id_fwd ls i =
-          do
-            ls0 <- id_mut_fwd ls;
-            list_nth_mut_loop_with_id_loop_fwd i ls0
-          od
-   
-   [list_nth_mut_loop_with_id_loop_back_def]  Definition
-      
-      ⊢ ∀i ls ret.
-          list_nth_mut_loop_with_id_loop_back i ls ret =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return (ListCons ret tl)
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  tl0 <- list_nth_mut_loop_with_id_loop_back i0 tl ret;
-                  Return (ListCons x tl0)
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_loop_with_id_loop_fwd_def]  Definition
-      
-      ⊢ ∀i ls.
-          list_nth_mut_loop_with_id_loop_fwd i ls =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return x
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  list_nth_mut_loop_with_id_loop_fwd i0 tl
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_shared_loop_pair_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_shared_loop_pair_back ls0 ls1 i ret =
-          list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret
-   
-   [list_nth_mut_shared_loop_pair_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_shared_loop_pair_fwd ls0 ls1 i =
-          list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i
-   
-   [list_nth_mut_shared_loop_pair_loop_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_shared_loop_pair_loop_back ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl0)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl00 <-
-                         list_nth_mut_shared_loop_pair_loop_back tl0 tl1 i0
-                           ret;
-                       Return (ListCons x0 tl00)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_shared_loop_pair_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_shared_loop_pair_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_mut_shared_loop_pair_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_shared_loop_pair_merge_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_shared_loop_pair_merge_back ls0 ls1 i ret =
-          list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret
-   
-   [list_nth_mut_shared_loop_pair_merge_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_shared_loop_pair_merge_fwd ls0 ls1 i =
-          list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-   
-   [list_nth_mut_shared_loop_pair_merge_loop_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_mut_shared_loop_pair_merge_loop_back ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl0)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl00 <-
-                         list_nth_mut_shared_loop_pair_merge_loop_back tl0
-                           tl1 i0 ret;
-                       Return (ListCons x0 tl00)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_mut_shared_loop_pair_merge_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_mut_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_mut_shared_loop_pair_merge_loop_fwd tl0 tl1
-                         i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls i.
-          list_nth_shared_loop_fwd ls i =
-          list_nth_shared_loop_loop_fwd ls i
-   
-   [list_nth_shared_loop_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls i.
-          list_nth_shared_loop_loop_fwd ls i =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return x
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  list_nth_shared_loop_loop_fwd tl i0
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_loop_pair_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_loop_pair_fwd ls0 ls1 i =
-          list_nth_shared_loop_pair_loop_fwd ls0 ls1 i
-   
-   [list_nth_shared_loop_pair_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_loop_pair_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_shared_loop_pair_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_loop_pair_merge_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_loop_pair_merge_fwd ls0 ls1 i =
-          list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i
-   
-   [list_nth_shared_loop_pair_merge_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_loop_pair_merge_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_shared_loop_pair_merge_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_loop_with_id_fwd_def]  Definition
-      
-      ⊢ ∀ls i.
-          list_nth_shared_loop_with_id_fwd ls i =
-          do
-            ls0 <- id_shared_fwd ls;
-            list_nth_shared_loop_with_id_loop_fwd i ls0
-          od
-   
-   [list_nth_shared_loop_with_id_loop_fwd_def]  Definition
-      
-      ⊢ ∀i ls.
-          list_nth_shared_loop_with_id_loop_fwd i ls =
-          case ls of
-            ListCons x tl =>
-              if i = int_to_u32 0 then Return x
-              else
-                do
-                  i0 <- u32_sub i (int_to_u32 1);
-                  list_nth_shared_loop_with_id_loop_fwd i0 tl
-                od
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_mut_loop_pair_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_shared_mut_loop_pair_back ls0 ls1 i ret =
-          list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret
-   
-   [list_nth_shared_mut_loop_pair_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_mut_loop_pair_fwd ls0 ls1 i =
-          list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i
-   
-   [list_nth_shared_mut_loop_pair_loop_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_shared_mut_loop_pair_loop_back ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl10 <-
-                         list_nth_shared_mut_loop_pair_loop_back tl0 tl1 i0
-                           ret;
-                       Return (ListCons x1 tl10)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_mut_loop_pair_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_mut_loop_pair_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_shared_mut_loop_pair_loop_fwd tl0 tl1 i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_mut_loop_pair_merge_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_shared_mut_loop_pair_merge_back ls0 ls1 i ret =
-          list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret
-   
-   [list_nth_shared_mut_loop_pair_merge_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_mut_loop_pair_merge_fwd ls0 ls1 i =
-          list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i
-   
-   [list_nth_shared_mut_loop_pair_merge_loop_back_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i ret.
-          list_nth_shared_mut_loop_pair_merge_loop_back ls0 ls1 i ret =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (ListCons ret tl1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       tl10 <-
-                         list_nth_shared_mut_loop_pair_merge_loop_back tl0
-                           tl1 i0 ret;
-                       Return (ListCons x1 tl10)
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [list_nth_shared_mut_loop_pair_merge_loop_fwd_def]  Definition
-      
-      ⊢ ∀ls0 ls1 i.
-          list_nth_shared_mut_loop_pair_merge_loop_fwd ls0 ls1 i =
-          case ls0 of
-            ListCons x0 tl0 =>
-              (case ls1 of
-                 ListCons x1 tl1 =>
-                   if i = int_to_u32 0 then Return (x0,x1)
-                   else
-                     do
-                       i0 <- u32_sub i (int_to_u32 1);
-                       list_nth_shared_mut_loop_pair_merge_loop_fwd tl0 tl1
-                         i0
-                     od
-               | ListNil => Fail Failure)
-          | ListNil => Fail Failure
-   
-   [sum_fwd_def]  Definition
-      
-      ⊢ ∀max. sum_fwd max = sum_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-   
-   [sum_loop_fwd_def]  Definition
-      
-      ⊢ ∀max i s.
-          sum_loop_fwd max i s =
-          if u32_lt i max then
-            do
-              s0 <- u32_add s i;
-              i0 <- u32_add i (int_to_u32 1);
-              sum_loop_fwd max i0 s0
-            od
-          else u32_mul s (int_to_u32 2)
-   
-   [sum_with_mut_borrows_fwd_def]  Definition
-      
-      ⊢ ∀max.
-          sum_with_mut_borrows_fwd max =
-          sum_with_mut_borrows_loop_fwd max (int_to_u32 0) (int_to_u32 0)
-   
-   [sum_with_mut_borrows_loop_fwd_def]  Definition
-      
-      ⊢ ∀max mi ms.
-          sum_with_mut_borrows_loop_fwd max mi ms =
-          if u32_lt mi max then
-            do
-              ms0 <- u32_add ms mi;
-              mi0 <- u32_add mi (int_to_u32 1);
-              sum_with_mut_borrows_loop_fwd max mi0 ms0
-            od
-          else u32_mul ms (int_to_u32 2)
-   
-   [sum_with_shared_borrows_fwd_def]  Definition
-      
-      ⊢ ∀max.
-          sum_with_shared_borrows_fwd max =
-          sum_with_shared_borrows_loop_fwd max (int_to_u32 0)
-            (int_to_u32 0)
-   
-   [sum_with_shared_borrows_loop_fwd_def]  Definition
-      
-      ⊢ ∀max i s.
-          sum_with_shared_borrows_loop_fwd max i s =
-          if u32_lt i max then
-            do
-              i0 <- u32_add i (int_to_u32 1);
-              s0 <- u32_add s i0;
-              sum_with_shared_borrows_loop_fwd max i0 s0
-            od
-          else u32_mul s (int_to_u32 2)
-   
-   
-*)
-end
diff --git a/tests/hol4/misc-loops/loops_TypesScript.sml b/tests/hol4/misc-loops/loops_TypesScript.sml
deleted file mode 100644
index e3e5b8d1..00000000
--- a/tests/hol4/misc-loops/loops_TypesScript.sml
+++ /dev/null
@@ -1,13 +0,0 @@
-(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
-(** [loops]: type definitions *)
-open primitivesLib divDefLib
-
-val _ = new_theory "loops_Types"
-
-
-Datatype:
-  (** [loops::List] *)
-  list_t = | ListCons 't list_t | ListNil
-End
-
-val _ = export_theory ()
diff --git a/tests/hol4/misc-loops/loops_TypesTheory.sig b/tests/hol4/misc-loops/loops_TypesTheory.sig
deleted file mode 100644
index c3e638d8..00000000
--- a/tests/hol4/misc-loops/loops_TypesTheory.sig
+++ /dev/null
@@ -1,94 +0,0 @@
-signature loops_TypesTheory =
-sig
-  type thm = Thm.thm
-  
-  (*  Definitions  *)
-    val list_t_TY_DEF : thm
-    val list_t_case_def : thm
-    val list_t_size_def : thm
-  
-  (*  Theorems  *)
-    val datatype_list_t : thm
-    val list_t_11 : thm
-    val list_t_Axiom : thm
-    val list_t_case_cong : thm
-    val list_t_case_eq : thm
-    val list_t_distinct : thm
-    val list_t_induction : thm
-    val list_t_nchotomy : thm
-  
-  val loops_Types_grammars : type_grammar.grammar * term_grammar.grammar
-(*
-   [divDef] Parent theory of "loops_Types"
-   
-   [list_t_TY_DEF]  Definition
-      
-      ⊢ ∃rep.
-          TYPE_DEFINITION
-            (λa0'.
-                 ∀ $var$('list_t').
-                   (∀a0'.
-                      (∃a0 a1.
-                         a0' =
-                         (λa0 a1.
-                              ind_type$CONSTR 0 a0
-                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
-                           a0 a1 ∧ $var$('list_t') a1) ∨
-                      a0' =
-                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
-                      $var$('list_t') a0') ⇒
-                   $var$('list_t') a0') rep
-   
-   [list_t_case_def]  Definition
-      
-      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
-        ∀f v. list_t_CASE ListNil f v = v
-   
-   [list_t_size_def]  Definition
-      
-      ⊢ (∀f a0 a1.
-           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
-        ∀f. list_t_size f ListNil = 0
-   
-   [datatype_list_t]  Theorem
-      
-      ⊢ DATATYPE (list_t ListCons ListNil)
-   
-   [list_t_11]  Theorem
-      
-      ⊢ ∀a0 a1 a0' a1'.
-          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
-   
-   [list_t_Axiom]  Theorem
-      
-      ⊢ ∀f0 f1. ∃fn.
-          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
-          fn ListNil = f1
-   
-   [list_t_case_cong]  Theorem
-      
-      ⊢ ∀M M' f v.
-          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
-          (M' = ListNil ⇒ v = v') ⇒
-          list_t_CASE M f v = list_t_CASE M' f' v'
-   
-   [list_t_case_eq]  Theorem
-      
-      ⊢ list_t_CASE x f v = v' ⇔
-        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
-   
-   [list_t_distinct]  Theorem
-      
-      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
-   
-   [list_t_induction]  Theorem
-      
-      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
-   
-   [list_t_nchotomy]  Theorem
-      
-      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
-   
-   
-*)
-end