rhi/quox
rhi/quox
1
0
Fork 0
Code Issues 15 Pull requests 1 Releases Wiki Activity

make IsQty interface

Browse source
This commit is contained in:
rhiannon morris 2021-09-09 23:51:45 +02:00
parent b47ef502f3
commit b29b7855a2
1 changed files with 25 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/Quox/Syntax/Qty.idr
View file

@ -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