Documentation

data T n a Source

type family Position n :: * Source

type family List n :: * -> * Source

type family Length f Source

data Index n Source

data Zero Source

data Succ pos Source

toList :: Natural n => T n a -> [a] Source

showsPrec :: (Natural n, Show a) => Int -> T n a -> ShowS Source

map :: Natural n => (a -> b) -> T n a -> T n b Source

zipWith :: Natural n => (a -> b -> c) -> T n a -> T n b -> T n c Source

sequenceA :: (Applicative f, Natural n) => T n (f a) -> f (T n a) Source

repeat :: Natural n => a -> T n a Source

index :: Natural n => Index n -> T n a -> a Source

update :: Natural n => (a -> a) -> Index n -> T n a -> T n a Source

indices :: Natural n => T n (Index n) Source

indicesInt :: Natural n => T n Int Source

numFromIndex :: Natural n => Index n -> Word Source

type GE1 n = Succ n Source

type GE2 n = Succ (GE1 n) Source

type GE3 n = Succ (GE2 n) Source

type GE4 n = Succ (GE3 n) Source

type GE5 n = Succ (GE4 n) Source

type GE6 n = Succ (GE5 n) Source

type GE7 n = Succ (GE6 n) Source

type GE8 n = Succ (GE7 n) Source

i0 :: Index (GE1 n) Source

i1 :: Index (GE2 n) Source

i2 :: Index (GE3 n) Source

i3 :: Index (GE4 n) Source

i4 :: Index (GE5 n) Source

i5 :: Index (GE6 n) Source

i6 :: Index (GE7 n) Source

i7 :: Index (GE8 n) Source

fromFixedList :: List n a -> T n a Source

toFixedList :: T n a -> List n a Source

(!:) :: a -> T n a -> T (Succ n) a infixr 5 Source

end :: T Zero a Source

singleton :: a -> T U1 a Source

viewL :: T (Succ n) a -> (a, T n a) Source

switchL :: (a -> T n a -> b) -> T (Succ n) a -> b Source

head :: Positive n => T n a -> a Source

tail :: T (Succ n) a -> T n a Source

switchEnd :: b -> T Zero a -> b Source

type family Curried n a b Source

uncurry :: Natural n => Curried n a b -> T n a -> b Source

minimum :: (Positive n, Ord a) => T n a -> a Source

maximum :: (Positive n, Ord a) => T n a -> a Source