From 982e7f89c54455656b449f803a57ea5d5a45f067 Mon Sep 17 00:00:00 2001
From: Hongwei <gmhwxi@gmail.com>
Date: Sun, 18 Aug 2024 15:33:24 -0400
Subject: [PATCH] Updating: very very minorly

---
 prelude/DATS/strn000.dats         | 27 ++++++++++++++++++++-------
 prelude/SATS/strn000.sats         | 25 ++++++++++++++++++++-----
 prelude/basics0.sats              |  7 +++++--
 srcgen1/prelude/SATS/xunimpl.sats | 13 +++++++++++++
 4 files changed, 58 insertions(+), 14 deletions(-)

diff --git a/prelude/DATS/strn000.dats b/prelude/DATS/strn000.dats
index 5f04849fa..790e6b2b5 100644
--- a/prelude/DATS/strn000.dats
+++ b/prelude/DATS/strn000.dats
@@ -153,12 +153,25 @@ end//let//end($UN.gasz_lget$at$raw<strn><cgtz>)
 //
 #impltmp
 <(*tmp*)>
+strn_slice
+(cs, i0, j0) =
+(
+strn_make_nfun<>
+(
+j0-i0,
+lam(k0) =>
+$UN.strn_get$at$raw<>(cs,i0+k0)
+)
+)//end-of-[strn_slice(cs,i0,j0)]
+//
+(* ****** ****** *)
+//
+#impltmp
+<(*tmp*)>
 strn_prefix
   (cs, i0) =
 (
-strn_make_nfun<>(i0,
-lam(j0) =>
-$UN.strn_get$at$raw<>(cs, j0)))
+  strn_slice<>(cs, 0, i0))
 //
 #impltmp
 <(*tmp*)>
@@ -167,12 +180,12 @@ strn_suffix
 let
 val n0 =
 strn_length<>(cs) in//let
-strn_make_nfun<>(n0-i0,
-lam(j0) =>
-$UN.strn_get$at$raw<>(cs, i0+j0))
-end//let//end-of-[strn_suffix(...)]
+(
+  strn_slice<>(cs, i0, n0)) end
+//let//end-of-[strn_suffix(cs,i0)]
 //
 (* ****** ****** *)
+(* ****** ****** *)
 //
 (*
 HX-2024-08-17:
diff --git a/prelude/SATS/strn000.sats b/prelude/SATS/strn000.sats
index 923a818b5..a411cc6a8 100644
--- a/prelude/SATS/strn000.sats
+++ b/prelude/SATS/strn000.sats
@@ -150,20 +150,35 @@ strn_gmake1(x: (!a)): (strn)
 (* ****** ****** *)
 //
 fun<>
+strn_slice
+{n0:i0}
+{i0:nat
+;j0:int
+|i0<=j0
+;j0<=n0}
+( cs: strn(n0)
+, i0: sint(i0)
+, j0: sint(j0)): strn(j0-i0)
+#symload
+slice with strn_slice of 1000
+//
+fun<>
 strn_prefix
 {n0:i0}
-{i0:i0|i0<=n0}
+{i0:nat
+|i0<=n0}
 ( cs: strn(n0)
 , i0: sint(i0)): strn(i0)
+#symload
+prefix with strn_prefix of 1000
+//
 fun<>
 strn_suffix
 {n0:i0}
-{i0:i0|i0<=n0}
+{i0:nat
+|i0<=n0}
 ( cs: strn(n0)
 , i0: sint(i0)): strn(n0-i0)
-//
-#symload
-prefix with strn_prefix of 1000
 #symload
 suffix with strn_suffix of 1000
 //
diff --git a/prelude/basics0.sats b/prelude/basics0.sats
index 4d0271b07..aecac11d1 100644
--- a/prelude/basics0.sats
+++ b/prelude/basics0.sats
@@ -380,10 +380,13 @@ neq_i0_i0: (i0, i0) -> b0
 //
 (* ****** ****** *)
 //
-#sortdef pos = {a:i0 | a > 0}
-#sortdef neg = {a:i0 | a < 0}
+#sortdef n0 = {a:i0 | a >= 0}
+//
+(* ****** ****** *)
 //
+#sortdef neg = {a:i0 | a < 0}
 #sortdef nat = {a:i0 | a >= 0}
+#sortdef pos = {a:i0 | a >= 1}
 //
 (* ****** ****** *)
 //
diff --git a/srcgen1/prelude/SATS/xunimpl.sats b/srcgen1/prelude/SATS/xunimpl.sats
index 9d1675b04..15c69db62 100644
--- a/srcgen1/prelude/SATS/xunimpl.sats
+++ b/srcgen1/prelude/SATS/xunimpl.sats
@@ -429,6 +429,19 @@ strn_gmake( a ): strn
 (* ****** ****** *)
 //
 fun<>
+strn_slice
+{n0:i0}
+{i0:nat
+;j0:int
+|i0<=j0
+;j0<=n0}
+( cs: strn(n0)
+, i0: sint(i0)
+, j0: sint(j0)): strn(j0-i0)
+#symload
+slice with strn_slice of 1000
+//
+fun<>
 strn_prefix
 {n0:i0}
 {i0:i0|i0<=n0}