Dinwiddy.Array

Definitions

Array : (dimension : Nat) -> Vect dimension Nat -> Type -> Type

  A type-safe array, based on Vect.
  Example usage:
  ```idris
  x : Array 3 [5, 5, 6] Bool
  ```
  Will create a 3-dimensional Array with the size of 5x5x6.
  
  As another example,
  ```
  x : Array 2 [2, 3] Bool
  ```
  Will create an array that looks like this:
  ```
  ###
  ###
  ```
  Full of booleans. It's value could be, for example:
  x = [[ True,  True,  True ],
       [ False, False, True ]]
  
  This type has an advantage over `UnsafeArray`, because it's
  indexed in the type like `Vect`s.

Visibility: public export