diff --git a/src/Quox/Syntax/Qty.idr b/src/Quox/Syntax/Qty.idr index 4689d2d..90c0783 100644 --- a/src/Quox/Syntax/Qty.idr +++ b/src/Quox/Syntax/Qty.idr @@ -6,14 +6,14 @@ import Data.Fin public export -data Qty = Zero | One | Many +data Qty = Zero | One | Any %name Qty.Qty pi, rh private Repr : Type Repr = Fin 3 private %inline repr : Qty -> Repr -repr pi = case pi of Zero => 0; One => 1; Many => 2 +repr pi = case pi of Zero => 0; One => 1; Any => 2 export Eq Qty where (==) = (==) `on` repr export Ord Qty where compare = compare `on` repr @@ -25,7 +25,7 @@ PrettyHL Qty where case pi of Zero => ifUnicode "𝟬" "0" One => ifUnicode "𝟭" "1" - Many => ifUnicode "𝛚" "*" + Any => ifUnicode "𝛚" "*" export %inline prettyQtyBinds : Pretty.HasEnv m => List Qty -> m (Doc HL) @@ -38,7 +38,7 @@ public export (+) : Qty -> Qty -> Qty Zero + rh = rh pi + Zero = pi -_ + _ = Many +_ + _ = Any public export (*) : Qty -> Qty -> Qty @@ -46,9 +46,9 @@ Zero * _ = Zero _ * Zero = Zero One * rh = rh pi * One = pi -Many * Many = Many +Any * Any = Any infix 6 <=. public export (<=.) : Qty -> Qty -> Bool -pi <=. rh = rh == Many || pi == rh +pi <=. rh = rh == Any || pi == rh