0 | module Dinwiddy.UnsafeArray
 1 |
 2 | ||| A type-unsafe array, based on List.
 3 | ||| Example usage:
 4 | ||| ```
 5 | ||| x : UnsafeArray 2 Int
 6 | ||| ```
 7 | ||| Will create a type for 2-dimensional infinite arrays.
 8 | ||| Please don't use this type, unless absolutely necessary,
 9 | ||| because lengths are not indexed in the type. This type is
10 | ||| based off of Idris' Lists.
11 | public export
12 | UnsafeArray : (dimension : Nat) -> (type : Type) -> Type
13 | UnsafeArray (S Z) t = List t
14 | UnsafeArray (S k) t = List (UnsafeArray k t)
15 | UnsafeArray Z     _ = ()
16 |