From b29b7855a2f45936b25e2bf37e1daf6cd22d21b8 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 9 Sep 2021 23:51:45 +0200
Subject: [PATCH] make IsQty interface

---
 src/Quox/Syntax/Qty.idr | 37 +++++++++++++++++++++++++------------
 1 file changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr
index 90c0783..3cec218 100644
--- a/src/Quox/Syntax/Qty.idr
+++ b/src/Quox/Syntax/Qty.idr
@@ -35,20 +35,33 @@ prettyQtyBinds =
 
 
 public export
-(+) : Qty -> Qty -> Qty
-Zero + rh   = rh
-pi   + Zero = pi
-_    + _    = Any
+plus : Qty -> Qty -> Qty
+plus Zero rh   = rh
+plus pi   Zero = pi
+plus _    _    = Any
 
 public export
-(*) : Qty -> Qty -> Qty
-Zero * _    = Zero
-_    * Zero = Zero
-One  * rh   = rh
-pi   * One  = pi
-Any  * Any  = Any
+times : Qty -> Qty -> Qty
+times Zero _    = Zero
+times _    Zero = Zero
+times One  rh   = rh
+times pi   One  = pi
+times Any  Any  = Any
 
 infix 6 <=.
 public export
-(<=.) : Qty -> Qty -> Bool
-pi <=. rh = rh == Any || pi == rh
+compat : Qty -> Qty -> Bool
+compat pi rh = rh == Any || pi == rh
+
+
+public export
+interface IsQty q where
+  zero, one : q
+  (+),  (*) : q -> q -> q
+  (<=.)     : q -> q -> Bool
+
+public export
+IsQty Qty where
+  zero  = Zero; one = One
+  (+)   = plus; (*) = times
+  (<=.) = compat