
  0 | |||This is a slightly modified copy of the same module from `contrib` package.
  1 | module TyRE.Text.Quantity
  2 | 
  3 | public export
  4 | record Quantity where
  5 |   constructor Qty
  6 |   min : Nat
  7 |   max : Maybe Nat
  8 | 
  9 | public export
 10 | Show Quantity where
 11 |   show (Qty Z Nothing) = "*"
 12 |   show (Qty Z (Just (S Z))) = "?"
 13 |   show (Qty (S Z) Nothing) = "+"
 14 |   show (Qty min max) = "{" ++ show min ++ showMax ++ "}"
 15 |     where
 16 |       showMax : String
 17 |       showMax = case max of
 18 |                      Nothing => ","
 19 |                      Just max' => if min == max'
 20 |                                      then ""
 21 |                                      else "," ++ show max'
 22 | 
 23 | public export
 24 | between : Nat -> Nat -> Quantity
 25 | between min max = Qty min (Just max)
 26 | 
 27 | public export
 28 | atLeast : Nat -> Quantity
 29 | atLeast min = Qty min Nothing
 30 | 
 31 | public export
 32 | atMost : Nat -> Quantity
 33 | atMost max = Qty 0 (Just max)
 34 | 
 35 | public export
 36 | exactly : Nat -> Quantity
 37 | exactly n = Qty n (Just n)
 38 | 
 39 | public export
 40 | inOrder : Quantity -> Bool
 41 | inOrder (Qty min Nothing) = True
 42 | inOrder (Qty min (Just max)) = min <= max
 43 |