Idris2Doc : Text.Quantity

Text.Quantity

record Quantity : Type
  Totality: total
  Constructor: 
Qty : Nat -> Maybe Nat -> Quantity

  Projections:
  
.max : Quantity -> Maybe Nat
  
.min : Quantity -> Nat
atLeast : Nat -> Quantity
  Totality: total
atMost : Nat -> Quantity
  Totality: total
between : Nat -> Nat -> Quantity
  Totality: total
exactly : Nat -> Quantity
  Totality: total
inOrder : Quantity -> Bool
  Totality: total