Text.Quantity

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

Totality: total
Visibility: public export

min : Quantity -> Nat

Totality: total
Visibility: public export

.max : Quantity -> Maybe Nat

Totality: total
Visibility: public export

max : Quantity -> Maybe Nat

Totality: total
Visibility: public export

between : Nat -> Nat -> Quantity

Totality: total
Visibility: public export

atLeast : Nat -> Quantity

Totality: total
Visibility: public export

atMost : Nat -> Quantity

Totality: total
Visibility: public export

exactly : Nat -> Quantity

Totality: total
Visibility: public export

inOrder : Quantity -> Bool

Totality: total
Visibility: public export