Copyright | (c) 2011 National Institute of Aerospace / Galois Inc. |
---|---|
Safe Haskell | Safe |
Language | Haskell2010 |
Copilot.Core.Type.Array
Description
Implementation of an array that uses type literals to store length. No explicit indexing is used for the input data. Supports arbitrary nesting of arrays.
Synopsis
- data Array (n :: Nat) t
- array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t
- arrayElems :: forall (n :: Nat) a. Array n a -> [a]
- arrayUpdate :: forall (n :: Nat) a. Array n a -> Int -> a -> Array n a
Documentation
data Array (n :: Nat) t Source #
Implementation of an array that uses type literals to store length.
array :: forall (n :: Nat) t. KnownNat n => [t] -> Array n t Source #
Smart array constructor that only type checks if the length of the given list matches the length of the array at type level.
arrayElems :: forall (n :: Nat) a. Array n a -> [a] Source #
Return the elements of an array.