module Text.Quantity %default total public exportrecord Quantity where  constructor Qty  min : Nat  max : Maybe Nat public exportShow Quantity where  show (Qty Z Nothing) = "*"  show (Qty Z (Just (S Z))) = "?"  show (Qty (S Z) Nothing) = "+"  show (Qty min max) = "{" ++ show min ++ showMax ++ "}"    where      showMax : String      showMax = case max of                     Nothing => ","                     Just max' => if min == max'                                     then ""                                     else "," ++ show max' public exportbetween : Nat -> Nat -> Quantitybetween min max = Qty min (Just max) public exportatLeast : Nat -> QuantityatLeast min = Qty min Nothing public exportatMost : Nat -> QuantityatMost max = Qty 0 (Just max) public exportexactly : Nat -> Quantityexactly n = Qty n (Just n) public exportinOrder : Quantity -> BoolinOrder (Qty min Nothing) = TrueinOrder (Qty min (Just max)) = min <= max