Data.FVect.Capacity

Definitions

data Capacity : Type -> Type

  A representation of the remaining capacity an FVect has for storage.
  A `Full` value has proof that there are `n` values in a vect with
  capacity `n`.
  A `NotFull` value has exactly what you need to cons an additional
  value onto an FVect.

Totality: total
Visibility: public export
Constructors:

Full : (0 _ : finToNat l = c) -> Capacity (FVect c l e)

NotFull : (0 _ : LT (finToNat len) (S n)) -> Capacity (FVect (S n) len e)

capacity : (0 _ : FVect c l e) -> Capacity (FVect c l e)

  Determine if the given FVect has more capacity for storage or not.

Visibility: export

capacity' : FVect c l e -> Capacity (FVect c l e)

  Calculate if the given FVect has more capacity for storage or not.

Visibility: export