TyRE.Text.Quantity

This is a slightly modified copy of the same module from `contrib` package.

Definitions

record Quantity : Type

Totality: total
Visibility: public export
Constructor: 

Qty : Nat -> Maybe Nat -> Quantity

Projections:

.max : Quantity -> Maybe Nat

.min : Quantity -> Nat

Hint: 

Show Quantity

.min : Quantity -> Nat

Visibility: public export

min : Quantity -> Nat

Visibility: public export

.max : Quantity -> Maybe Nat

Visibility: public export

max : Quantity -> Maybe Nat

Visibility: public export

between : Nat -> Nat -> Quantity

Visibility: public export

atLeast : Nat -> Quantity

Visibility: public export

atMost : Nat -> Quantity

Visibility: public export

exactly : Nat -> Quantity

Visibility: public export

inOrder : Quantity -> Bool

Visibility: public export