From 82795e997633987b570ee969aa230fba60f13c59 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Mon, 9 Jan 2023 23:43:55 +0100
Subject: [PATCH] remove IsOne stuff; add timesSubj

---
 lib/Quox/Syntax/Qty.idr       |  8 +-------
 lib/Quox/Syntax/Qty/Three.idr | 12 ++++++++----
 2 files changed, 9 insertions(+), 11 deletions(-)

diff --git a/lib/Quox/Syntax/Qty.idr b/lib/Quox/Syntax/Qty.idr
index f80e703..727ae4a 100644
--- a/lib/Quox/Syntax/Qty.idr
+++ b/lib/Quox/Syntax/Qty.idr
@@ -30,12 +30,6 @@ interface Eq q => IsQty q where
   isZero : Dec1 IsZero
   zeroIsZero : IsZero zero
 
-  ||| true if bindings of this quantity must be linear
-  -- [fixme] is this needed for anything?
-  IsOne : Pred q
-  isOne : Dec1 IsOne
-  oneIsOne : IsOne one
-
   ||| ``p `Compat` q`` if it is ok for a binding of
   ||| quantity `q` to be used exactly `p` times.
   ||| e.g. ``1 `Compat` 1``, ``1 `Compat` ω``
@@ -49,6 +43,7 @@ interface Eq q => IsQty q where
   isSubj : Dec1 IsSubj
   zeroIsSubj : IsSubj zero
   oneIsSubj  : IsSubj one
+  timesSubj  : forall pi, rh. IsSubj pi -> IsSubj rh -> IsSubj (pi * rh)
 
   ||| true if it is ok for a global definition to have this
   ||| quantity. so not exact usage counts, maybe.
@@ -75,4 +70,3 @@ GQty q = Subset q IsGlobal
 public export %inline
 gzero : IsQty q => GQty q
 gzero = Element zero zeroIsGlobal
-
diff --git a/lib/Quox/Syntax/Qty/Three.idr b/lib/Quox/Syntax/Qty/Three.idr
index d2a7538..d0d6033 100644
--- a/lib/Quox/Syntax/Qty/Three.idr
+++ b/lib/Quox/Syntax/Qty/Three.idr
@@ -65,6 +65,13 @@ isSubj3 Zero = Yes SZero
 isSubj3 One  = Yes SOne
 isSubj3 Any  = No $ \case _ impossible
 
+public export
+timesSubj3 : forall pi, rh. IsSubj3 pi -> IsSubj3 rh -> IsSubj3 (times pi rh)
+timesSubj3 SZero SZero = SZero
+timesSubj3 SZero SOne  = SZero
+timesSubj3 SOne  SZero = SZero
+timesSubj3 SOne  SOne  = SOne
+
 
 public export
 data IsGlobal3 : Pred Three where
@@ -89,10 +96,6 @@ IsQty Three where
   isZero     = decEq Zero
   zeroIsZero = Refl
 
-  IsOne    = Equal One
-  isOne    = decEq One
-  oneIsOne = Refl
-
   Compat = Compat3
   compat = compat3
 
@@ -100,6 +103,7 @@ IsQty Three where
   isSubj     = isSubj3
   zeroIsSubj = SZero
   oneIsSubj  = SOne
+  timesSubj  = timesSubj3
 
   IsGlobal     = IsGlobal3
   isGlobal     = isGlobal3