From 25521e106c9fecdf200d9e729c891136671abcde Mon Sep 17 00:00:00 2001
From: Hongwei <gmhwxi@gmail.com>
Date: Fri, 13 Sep 2024 23:43:32 -0400
Subject: [PATCH] Updating: very very minorly

---
 prelude/DATS/VT/list000_vt.dats |  4 ---
 prelude/DATS/optn000.dats       | 45 ++++++++++++++++++-------------
 prelude/SATS/VT/list000_vt.sats | 48 ++++++++++++++++++++++++++-------
 3 files changed, 65 insertions(+), 32 deletions(-)

diff --git a/prelude/DATS/VT/list000_vt.dats b/prelude/DATS/VT/list000_vt.dats
index 2fb333175..e04e9c2b8 100644
--- a/prelude/DATS/VT/list000_vt.dats
+++ b/prelude/DATS/VT/list000_vt.dats
@@ -333,10 +333,6 @@ end // end of [list_vt_cons(...)]
 list_vt_reverse0(xs) =
 list_vt_rappend00<a>(xs, list_vt_nil(*void*))
 //
-#impltmp
-< a: vt >
-list_vt_rappend0 = list_vt_rappend00<a>(*void*)
-//
 (* ****** ****** *)
 (* ****** ****** *)
 //
diff --git a/prelude/DATS/optn000.dats b/prelude/DATS/optn000.dats
index 3a43743d1..294fe1d78 100644
--- a/prelude/DATS/optn000.dats
+++ b/prelude/DATS/optn000.dats
@@ -60,6 +60,17 @@ g_ptype<t0>((*0*)); pstrn(")"))
 (* ****** ****** *)
 //
 #impltmp
+{ x0:t0 }
+gseq_nil
+<optn(x0)><x0>
+  ((*void*)) =
+(
+  optn_nil((*0*)))
+//
+(* ****** ****** *)
+(* ****** ****** *)
+//
+#impltmp
 <(*tmp*)>
 optn_nil_
  ((*0*)) = optn_nil()
@@ -69,6 +80,7 @@ optn_cons_
  (  x0  ) = optn_cons(x0)
 //
 (* ****** ****** *)
+(* ****** ****** *)
 //
 #impltmp
 < (*0*) >
@@ -79,6 +91,12 @@ case+ xs of
 | optn_nil() => true
 | optn_cons(_) => false)
 //
+#impltmp
+{ x0:t0 }
+gseq_nilq
+<optn(x0)><x0> =
+optn_nilq<>{x0}(* void *)
+//
 (* ****** ****** *)
 (* ****** ****** *)
 //
@@ -90,24 +108,10 @@ optn_head
 case+ xs of
 | optn_cons(x0) => (x0))
 //
-(* ****** ****** *)
-(* ****** ****** *)
-//
 #impltmp
 { x0:t0 }
-gseq_nil
-<optn(x0)><x0>
-  ((*void*)) =
-(
-  optn_nil((*0*)))
-//
-(* ****** ****** *)
-//
-#impltmp
-{ x0:t0 }
-gseq_nilq
-<optn(x0)><x0>
- (  xs  ) = optn_nilq{x0}(xs)
+gseq_head
+<optn(x0)><x0> = optn_nilq<x0>
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -161,8 +165,13 @@ optn_length
   (xs) =
 (
 case+ xs of
-|
-optn_nil() => 0 | optn_cons _ => 1)
+| optn_nil() => 0
+| optn_cons(_, _) => 1)//impl
+//
+#impltmp
+{ x0:t0 }
+gseq_length
+<optn(x0)><x0> = optn_length<x0>
 //
 (* ****** ****** *)
 (* ****** ****** *)
diff --git a/prelude/SATS/VT/list000_vt.sats b/prelude/SATS/VT/list000_vt.sats
index e6f1d6b6f..535ed5bd7 100644
--- a/prelude/SATS/VT/list000_vt.sats
+++ b/prelude/SATS/VT/list000_vt.sats
@@ -119,6 +119,11 @@ list_vt_length1
 {n0:i0}
 (xs: !list_vt(x0,n0)): sint(n0)
 //
+#symload
+length0 with list_vt_length0 of 1000
+#symload
+length1 with list_vt_length1 of 1000
+//
 (* ****** ****** *)
 (* ****** ****** *)
 //
@@ -130,7 +135,7 @@ fun
 <x0:vt>
 list_vt_make0_lstrq
 {n0:i0}
-(xs: strq_vt(x0, n0)): list_vt(x0, n0)
+(xs: strq_vt(x0,n0)): list_vt(x0,n0)
 //
 #symload
 llist_make0 with list_vt_make0_lstrm
@@ -144,7 +149,10 @@ fun
 <x0:vt>
 list_vt_copy
  {n0:i0}
-( xs: ~list_vt(x0,n0)): list_vt(x0,n0)
+( xs
+: !list_vt(x0,n0)): list_vt(x0,n0)
+//
+#symload copy with list_vt_copy of 1000
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -153,21 +161,27 @@ fun
 <x0:vt>
 list_vt_append0
 {n1,n2:i0}
-( xs: ~list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: ~list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 fun
 <x0:vt>
 list_vt_append00
 {n1,n2:i0}
-( xs: ~list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: ~list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 //
 fun
 <x0:vt>
 list_vt_append10
 {n1,n2:i0}
-( xs: !list_vt(x0,n1)
-, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+( xs
+: !list_vt(x0,n1)
+, ys
+: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 //
 (* ****** ****** *)
 //
@@ -176,22 +190,29 @@ fun
 list_vt_reverse0
 {n0:i0}
 (xs: ~list_vt(x0,n0)): list_vt(x0,n0)
-//
 fun
 <x0:vt>
 list_vt_reverse1
 {n0:i0}
 (xs: !list_vt(x0,n0)): list_vt(x0,n0)
 //
+#symload reverse0 with list_reverse0 of 1000
+#symload reverse1 with list_reverse1 of 1000
+//
 (* ****** ****** *)
 //
 fun
 <x0:vt>
+list_vt_rappend0
+{n1,n2:i0}
+( xs: ~list_vt(x0,n1)
+, ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
+fun
+<x0:vt>
 list_vt_rappend00
 {n1,n2:i0}
 ( xs: ~list_vt(x0,n1)
 , ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
-//
 fun
 <x0:vt>
 list_vt_rappend10
@@ -199,6 +220,10 @@ list_vt_rappend10
 ( xs: !list_vt(x0,n1)
 , ys: ~list_vt(x0,n2)): list_vt(x0,n1+n2)
 //
+#symload rappend0 with list_rappend0 of 1000
+#symload rappend00 with list_rappend00 of 1000
+#symload rappend10 with list_rappend10 of 1000
+//
 (* ****** ****** *)
 (* ****** ****** *)
 //
@@ -208,6 +233,9 @@ GLSEQ_make0_list_vt
 (xs: list_vt(a)): GLSEQ(list_vt(a), a)
 #symload GLSEQ with GLSEQ_make0_list_vt of 1000
 //
+(* ****** ****** *)
+(* ****** ****** *)
+//
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)
 (* ****** ****** *)(* ****** ****** *)(* ****** ****** *)