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 t. KnownNat n => [t] -> Array n t
arrayElems :: Array n a -> [a]

Documentation

data Array (n :: Nat) t Source #

Implementation of an array that uses type literals to store length.

Instances

Instances details

Show t => Show (Array n t) Source #
Instance details Defined in Copilot.Core.Type.Array Methods showsPrec :: Int -> Array n t -> ShowS # show :: Array n t -> String # showList :: [Array n t] -> ShowS #
(Typeable t, Typed t, KnownNat n) => Typed (Array n t) Source #
Instance details Defined in Copilot.Core.Type Methods typeOf :: Type (Array n t) Source # simpleType :: Type (Array n t) -> SimpleType Source #

array :: forall n 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 :: Array n a -> [a] Source #

Return the elements of an array.