remove IsOne stuff; add timesSubj

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
-

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