Idris2Doc : Text.Quantity

Text.Quantity

(source)
Definitions
record Quantity : Type
  A quantity bounded by a minimum and, optionally, a maximum.
  It can be used in certain lexers or parsers to specify
  how many times an item is expected to appear.

  Totality: total
  Visibility: public export
  Constructor: 
Qty : Nat -> Maybe Nat -> Quantity

  Projections:
  
.max : Quantity -> Maybe Nat
  Optional maximum number of occurrences.
  
.min : Quantity -> Nat
  Minimum number of occurrences.

  Hint: 
Show Quantity
.min : Quantity -> Nat
  Minimum number of occurrences.

  Totality: total
  Visibility: public export
min : Quantity -> Nat
  Minimum number of occurrences.

  Totality: total
  Visibility: public export
.max : Quantity -> Maybe Nat
  Optional maximum number of occurrences.

  Totality: total
  Visibility: public export
max : Quantity -> Maybe Nat
  Optional maximum number of occurrences.

  Totality: total
  Visibility: public export
between : Nat -> Nat -> Quantity
  Create a `Quantity` with the given lower and upper bounds. {min,max}

  Totality: total
  Visibility: public export
atLeast : Nat -> Quantity
  Create a `Quantity` with only a lower bound. {min,}

  Totality: total
  Visibility: public export
atMost : Nat -> Quantity
  Create a `Quantity` from zero to the given upper bound. {0,max}

  Totality: total
  Visibility: public export
exactly : Nat -> Quantity
  Create a `Quantity` requiring an exact number of occurrences. {n}

  Totality: total
  Visibility: public export
inOrder : Quantity -> Bool
  Check whether a `Quantity`'s bounds are well-formed, i.e. min <= max.

  Totality: total
  Visibility: public export