Updating: very very minorly

githwxi · Dec 25, 2024 · d8fc848 · d8fc848
1 parent 174c7e0
commit d8fc848
Show file tree

Hide file tree

Showing 10 changed files with 440 additions and 440 deletions.
diff --git a/prelude/DATS/gasz001.dats b/prelude/DATS/gasz001.dats
@@ -184,14 +184,14 @@ end//let//end-of-[gasz_forall(xs)]
 #impltmp
 < xs:t0 >
 < x0:vt >
-gasz_forall_f1un
+gasz_forall$f1un
   (xs, test) =
 (
 gasz_forall
 <xs><x0>(xs)) where {
 #impltmp
 forall$test1<x0>(x0) = test(x0)//impl
-}(*where*)//end-of-[gasz_forall_f1un(xs)]
+}(*where*)//end-of-[gasz_forall$f1un(xs)]
 //
 (* ****** ****** *)
 //
@@ -213,14 +213,14 @@ end//let//end-of-[gasz_exists(xs)]
 #impltmp
 < xs:t0 >
 < x0:vt >
-gasz_exists_f1un
+gasz_exists$f1un
   (xs, test) =
 (
 gasz_exists
 <xs><x0>(xs)) where {
 #impltmp
 exists$test1<x0>(x0) = test(x0)//impl
-}(*where*)//end-of-[gasz_exists_f1un(xs)]
+}(*where*)//end-of-[gasz_exists$f1un(xs)]
 //
 (* ****** ****** *)
 //
@@ -265,15 +265,15 @@ end//let//end-of-[gasz_rforall(xs)]
 #impltmp
 < xs:t0 >
 < x0:vt >
-gasz_rforall_f1un
+gasz_rforall$f1un
   (xs, test) =
 (
 gasz_rforall
 <xs><x0>(xs)) where
 {
 #impltmp
 rforall$test1<x0>(x0) = test(x0)//impl
-}(*where*)//end-of-[gasz_rforall_f1un(xs)]
+}(*where*)//end-of-[gasz_rforall$f1un(xs)]
 //
 (* ****** ****** *)
 //
@@ -295,14 +295,14 @@ end//let//end-of-[gasz_rexists(xs)]
 #impltmp
 < xs:t0 >
 < x0:vt >
-gasz_rexists_f1un
+gasz_rexists$f1un
   (xs, test) =
 (
 gasz_rexists
 <xs><x0>(xs)) where {
 #impltmp
 rexists$test1<x0>(x0) = test(x0)//impl
-}(*where*)//end-of-[gasz_rexists_f1un(xs)]
+}(*where*)//end-of-[gasz_rexists$f1un(xs)]
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/DATS/gcls000.dats b/prelude/DATS/gcls000.dats
@@ -196,58 +196,58 @@ gseq_irforall<xs><x0>(GSEQ_unmk(gseq)))
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_forall_f1un
+GSEQ_forall$f1un
   (gseq, test) =
 (
-gseq_forall_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_forall$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_exists_f1un
+GSEQ_exists$f1un
   (gseq, test) =
 (
-gseq_exists_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_exists$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_rforall_f1un
+GSEQ_rforall$f1un
   (gseq, test) =
 (
-gseq_rforall_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_rforall$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_rexists_f1un
+GSEQ_rexists$f1un
   (gseq, test) =
 (
-gseq_rexists_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_rexists$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_iforall_f2un
+GSEQ_iforall$f2un
   (gseq, test) =
 (
-gseq_iforall_f2un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_iforall$f2un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_irforall_f2un
+GSEQ_irforall$f2un
   (gseq, test) =
 (
-gseq_irforall_f2un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_irforall$f2un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -289,34 +289,34 @@ gseq_irforitm<xs><x0>(GSEQ_unmk(gseq)))
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_foritm_f1un
+GSEQ_foritm$f1un
   (gseq, test) =
 (
-gseq_foritm_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_foritm$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_rforitm_f1un
+GSEQ_rforitm$f1un
   (gseq, test) =
 (
-gseq_rforitm_f1un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_rforitm$f1un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_iforitm_f2un
+GSEQ_iforitm$f2un
   (gseq, test) =
 (
-gseq_iforitm_f2un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_iforitm$f2un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
-GSEQ_irforitm_f2un
+GSEQ_irforitm$f2un
   (gseq, test) =
 (
-gseq_irforitm_f2un<xs><x0>(GSEQ_unmk(gseq), test))
+gseq_irforitm$f2un<xs><x0>(GSEQ_unmk(gseq), test))
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -363,37 +363,37 @@ gseq_irfolditm<xs><x0><r0>(GSEQ_unmk(gseq), r0))
 < xs:t0 >
 < x0:t0 >
 < r0:vt >
-GSEQ_folditm_f2un
+GSEQ_folditm$f2un
  (gseq, r0, fopr) =
 (
-gseq_folditm_f2un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
+gseq_folditm$f2un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
 < r0:vt >
-GSEQ_rfolditm_f2un
+GSEQ_rfolditm$f2un
  (gseq, r0, fopr) =
 (
-gseq_rfolditm_f2un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
+gseq_rfolditm$f2un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
 < r0:vt >
-GSEQ_ifolditm_f3un
+GSEQ_ifolditm$f3un
  (gseq, r0, fopr) =
 (
-gseq_ifolditm_f3un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
+gseq_ifolditm$f3un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
 //
 #impltmp
 < xs:t0 >
 < x0:t0 >
 < r0:vt >
-GSEQ_irfolditm_f3un
+GSEQ_irfolditm$f3un
  (gseq, r0, fopr) =
 (
-gseq_irfolditm_f3un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
+gseq_irfolditm$f3un<xs><x0><r0>(GSEQ_unmk(gseq), r0, fopr))
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -490,41 +490,41 @@ gasz_irforall<xs><x0>(GASZ_unmk(gasz)))
 #impltmp
 < xs:t0 >
 < x0:vt >
-GASZ_forall_f1un
+GASZ_forall$f1un
   (gasz, test) =
 (
-gasz_forall_f1un<xs><x0>(GASZ_unmk(gasz), test))
+gasz_forall$f1un<xs><x0>(GASZ_unmk(gasz), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:vt >
-GASZ_rforall_f1un
+GASZ_rforall$f1un
   (gasz, test) =
 (
-gasz_rforall_f1un<xs><x0>(GASZ_unmk(gasz), test))
+gasz_rforall$f1un<xs><x0>(GASZ_unmk(gasz), test))
 //
 (* ****** ****** *)
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:vt >
-GASZ_exists_f1un
+GASZ_exists$f1un
   (gasz, test) =
 (
-gasz_exists_f1un<xs><x0>(GASZ_unmk(gasz), test))
+gasz_exists$f1un<xs><x0>(GASZ_unmk(gasz), test))
 //
 (* ****** ****** *)
 //
 #impltmp
 < xs:t0 >
 < x0:vt >
-GASZ_rexists_f1un
+GASZ_rexists$f1un
   (gasz, test) =
 (
-gasz_rexists_f1un<xs><x0>(GASZ_unmk(gasz), test))
+gasz_rexists$f1un<xs><x0>(GASZ_unmk(gasz), test))
 //
 (* ****** ****** *)
 (* ****** ****** *)
@@ -548,10 +548,10 @@ gseq_foritm<xs><x0>(GASZ_unmk(gasz))
 #impltmp
 { xs:t0
 , x0:t0 }
-gseq_foritm_f1un
+gseq_foritm$f1un
 <GASZ(xs,x0)><x0>
  (gasz, test) =
-gseq_foritm_f1un<xs><x0>(GASZ_unmk(gasz), test)
+gseq_foritm$f1un<xs><x0>(GASZ_unmk(gasz), test)
 //
 (* ****** ****** *)
 //
@@ -566,10 +566,10 @@ gseq_rforitm<xs><x0>(GASZ_unmk(gasz))
 #impltmp
 { xs:t0
 , x0:t0 }
-gseq_rforitm_f1un
+gseq_rforitm$f1un
 <GASZ(xs,x0)><x0>
  (gasz, test) =
-gseq_rforitm_f1un<xs><x0>(GASZ_unmk(gasz), test)
+gseq_rforitm$f1un<xs><x0>(GASZ_unmk(gasz), test)
 //
 (* ****** ****** *)
 //
@@ -584,10 +584,10 @@ gseq_iforitm<xs><x0>(GASZ_unmk(gasz))
 #impltmp
 { xs:t0
 , x0:t0 }
-gseq_iforitm_f2un
+gseq_iforitm$f2un
 <GASZ(xs,x0)><x0>
  (gasz, test) =
-gseq_iforitm_f2un<xs><x0>(GASZ_unmk(gasz), test)
+gseq_iforitm$f2un<xs><x0>(GASZ_unmk(gasz), test)
 //
 (* ****** ****** *)
 //
@@ -602,10 +602,10 @@ gseq_irforitm<xs><x0>(GASZ_unmk(gasz))
 #impltmp
 { xs:t0
 , x0:t0 }
-gseq_irforitm_f2un
+gseq_irforitm$f2un
 <GASZ(xs,x0)><x0>
  (gasz, test) =
-gseq_irforitm_f2un<xs><x0>(GASZ_unmk(gasz), test)
+gseq_irforitm$f2un<xs><x0>(GASZ_unmk(gasz), test)
 //
 (* ****** ****** *)
 (* ****** ****** *)

diff --git a/prelude/DATS/gseq000.dats b/prelude/DATS/gseq000.dats
@@ -182,8 +182,8 @@ gseq_fmake_fwork<xs><x0>
 (
 lam(work) =>
 (
-gseq_foritm_f1un<xs><x0>(xs, work);
-gseq_foritm0_f1un<ys><x0>(ys, work)))
+gseq_foritm$f1un<xs><x0>(xs, work);
+gseq_foritm0$f1un<ys><x0>(ys, work)))
 //
 (* ****** ****** *)
 //
@@ -211,8 +211,8 @@ gseq_fmake_fwork<xs><x0>
 (
 lam(work) =>
 (
-gseq_foritm0_f1un<ys><x0>(ys, work)
-;gseq_foritm_f1un<xs><x0>(xs, work)))
+gseq_foritm0$f1un<ys><x0>(ys, work)
+;gseq_foritm$f1un<xs><x0>(xs, work)))
 //
 (* ****** ****** *)
 //
@@ -244,7 +244,7 @@ gseq_fmake_fwork<xs><x0>
 (
 lam(work) =>
 (
-gseq_rforitm_f1un<xs><x0>(xs, work)))
+gseq_rforitm$f1un<xs><x0>(xs, work)))
 //
 #impltmp
 < xs:t0 >
@@ -256,8 +256,8 @@ gseq_fmake_fwork<xs><x0>
 (
 lam(work) =>
 (
-gseq_rforitm_f1un<xs><x0>(xs, work);
-gseq_foritm0_f1un<ys><x0>(ys, work)))
+gseq_rforitm$f1un<xs><x0>(xs, work);
+gseq_foritm0$f1un<ys><x0>(ys, work)))
 //
 (* ****** ****** *)
 (* ****** ****** *)