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