Data.Fin.List

Lists of statically-known length

Documentation

data Peano

Instances

Bounded Peano

Defined in Data.Peano

Methods

minBound :: Peano

maxBound :: Peano

Enum Peano

Defined in Data.Peano

Methods

succ :: Peano -> Peano

pred :: Peano -> Peano

toEnum :: Int -> Peano

fromEnum :: Peano -> Int

enumFrom :: Peano -> [Peano]

enumFromThen :: Peano -> Peano -> [Peano]

enumFromTo :: Peano -> Peano -> [Peano]

enumFromThenTo :: Peano -> Peano -> Peano -> [Peano]

Eq Peano

Defined in Data.Peano

Methods

(==) :: Peano -> Peano -> Bool

(/=) :: Peano -> Peano -> Bool

Integral Peano

Defined in Data.Peano

Methods

quot :: Peano -> Peano -> Peano

rem :: Peano -> Peano -> Peano

div :: Peano -> Peano -> Peano

mod :: Peano -> Peano -> Peano

quotRem :: Peano -> Peano -> (Peano, Peano)

divMod :: Peano -> Peano -> (Peano, Peano)

toInteger :: Peano -> Integer

Data Peano

Defined in Data.Peano

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Peano -> c Peano

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Peano

toConstr :: Peano -> Constr

dataTypeOf :: Peano -> DataType

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Peano)

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Peano)

gmapT :: (forall b. Data b => b -> b) -> Peano -> Peano

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Peano -> r

gmapQ :: (forall d. Data d => d -> u) -> Peano -> [u]

gmapQi :: Int -> (forall d. Data d => d -> u) -> Peano -> u

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Peano -> m Peano

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Peano -> m Peano

Num Peano

Defined in Data.Peano

Methods

(+) :: Peano -> Peano -> Peano

(-) :: Peano -> Peano -> Peano

(*) :: Peano -> Peano -> Peano

negate :: Peano -> Peano

abs :: Peano -> Peano

signum :: Peano -> Peano

fromInteger :: Integer -> Peano

Ord Peano

Defined in Data.Peano

Methods

compare :: Peano -> Peano -> Ordering

(<) :: Peano -> Peano -> Bool

(<=) :: Peano -> Peano -> Bool

(>) :: Peano -> Peano -> Bool

(>=) :: Peano -> Peano -> Bool

max :: Peano -> Peano -> Peano

min :: Peano -> Peano -> Peano

Read Peano

Defined in Data.Peano

Methods

readsPrec :: Int -> ReadS Peano

readList :: ReadS [Peano]

readPrec :: ReadPrec Peano

readListPrec :: ReadPrec [Peano]

Real Peano

Defined in Data.Peano

Methods

toRational :: Peano -> Rational

Show Peano

Defined in Data.Peano

Methods

showsPrec :: Int -> Peano -> ShowS

show :: Peano -> String

showList :: [Peano] -> ShowS

Ix Peano

Defined in Data.Peano

Methods

range :: (Peano, Peano) -> [Peano]

index :: (Peano, Peano) -> Peano -> Int

unsafeIndex :: (Peano, Peano) -> Peano -> Int

inRange :: (Peano, Peano) -> Peano -> Bool

rangeSize :: (Peano, Peano) -> Int

unsafeRangeSize :: (Peano, Peano) -> Int

data List n a where

A list of exactly n values of type a

Constructors

Nil :: List Zero a

(:.) :: a -> List n a -> List (Succ n) a infixr 5

Instances

Functor (List n)

Defined in Data.Fin.Private

Methods

fmap :: (a -> b) -> List n a -> List n b

(<$) :: a -> List n b -> List n a

Natural n => Applicative (List n)

Defined in Data.Fin.Private

Methods

pure :: a -> List n a

(<*>) :: List n (a -> b) -> List n a -> List n b

liftA2 :: (a -> b -> c) -> List n a -> List n b -> List n c

(*>) :: List n a -> List n b -> List n b

(<*) :: List n a -> List n b -> List n a

Foldable (List n)

Defined in Data.Fin.Private

Methods

fold :: Monoid m => List n m -> m

foldMap :: Monoid m => (a -> m) -> List n a -> m

foldMap' :: Monoid m => (a -> m) -> List n a -> m

foldr :: (a -> b -> b) -> b -> List n a -> b

foldr' :: (a -> b -> b) -> b -> List n a -> b

foldl :: (b -> a -> b) -> b -> List n a -> b

foldl' :: (b -> a -> b) -> b -> List n a -> b

foldr1 :: (a -> a -> a) -> List n a -> a

foldl1 :: (a -> a -> a) -> List n a -> a

toList :: List n a -> [a]

null :: List n a -> Bool

length :: List n a -> Int

elem :: Eq a => a -> List n a -> Bool

maximum :: Ord a => List n a -> a

minimum :: Ord a => List n a -> a

sum :: Num a => List n a -> a

product :: Num a => List n a -> a

Traversable (List n)

Defined in Data.Fin.Private

Methods

traverse :: Applicative f => (a -> f b) -> List n a -> f (List n b)

sequenceA :: Applicative f => List n (f a) -> f (List n a)

mapM :: Monad m => (a -> m b) -> List n a -> m (List n b)

sequence :: Monad m => List n (m a) -> m (List n a)

Eq1 (List n)

Defined in Data.Fin.Private

Methods

liftEq :: (a -> b -> Bool) -> List n a -> List n b -> Bool

Ord1 (List n)

Defined in Data.Fin.Private

Methods

liftCompare :: (a -> b -> Ordering) -> List n a -> List n b -> Ordering

Natural n => Read1 (List n)

Defined in Data.Fin.Private

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (List n a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [List n a]

liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (List n a)

liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [List n a]

Show1 (List n)

Defined in Data.Fin.Private

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> List n a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [List n a] -> ShowS

Natural n => Foldable1 (List ('Succ n))

Defined in Data.Fin.Private

Methods

fold1 :: Semigroup a => List ('Succ n) a -> a

foldMap1 :: Semigroup b => (a -> b) -> List ('Succ n) a -> b

foldr1 :: (a -> a -> a) -> List ('Succ n) a -> a

foldl1 :: (a -> a -> a) -> List ('Succ n) a -> a

foldr1' :: (a -> a -> a) -> List ('Succ n) a -> a

foldl1' :: (a -> a -> a) -> List ('Succ n) a -> a

toNonEmpty :: List ('Succ n) a -> NonEmpty a

maximum :: Ord a => List ('Succ n) a -> a

minimum :: Ord a => List ('Succ n) a -> a

Eq a => Eq (List n a)

Defined in Data.Fin.Private

Methods

(==) :: List n a -> List n a -> Bool

(/=) :: List n a -> List n a -> Bool

Ord a => Ord (List n a)

Defined in Data.Fin.Private

Methods

compare :: List n a -> List n a -> Ordering

(<) :: List n a -> List n a -> Bool

(<=) :: List n a -> List n a -> Bool

(>) :: List n a -> List n a -> Bool

(>=) :: List n a -> List n a -> Bool

max :: List n a -> List n a -> List n a

min :: List n a -> List n a -> List n a

(Read a, Natural n) => Read (List n a)

Defined in Data.Fin.Private

Methods

readsPrec :: Int -> ReadS (List n a)

readList :: ReadS [List n a]

readPrec :: ReadPrec (List n a)

readListPrec :: ReadPrec [List n a]

Show a => Show (List n a)

Defined in Data.Fin.Private

Methods

showsPrec :: Int -> List n a -> ShowS

show :: List n a -> String

showList :: [List n a] -> ShowS

Semigroup a => Semigroup (List n a)

Defined in Data.Fin.Private

Methods

(<>) :: List n a -> List n a -> List n a

sconcat :: NonEmpty (List n a) -> List n a

stimes :: Integral b => b -> List n a -> List n a

(Natural n, Monoid a) => Monoid (List n a)

Defined in Data.Fin.Private

Methods

mempty :: List n a

mappend :: List n a -> List n a -> List n a

mconcat :: [List n a] -> List n a

fromList :: Natural n => [a] -> Maybe (List n a)

uncons :: List (Succ n) a -> (a, List n a)

head :: List (Succ n) a -> a

tail :: List (Succ n) a -> List n a

init :: List (Succ n) a -> List n a

last :: List (Succ n) a -> a

reverse :: List n a -> List n a

rotate :: Fin n -> List n a -> List n a

Bring givenly many elements from the tail of the list to the front.

at :: Functor f => Fin n -> (a -> f a) -> List n a -> f (List n a)

Focalize on the giventh element.

swap :: Fin n -> Fin n -> List n a -> List n a

Swap the 2 giventh elements of the list.

(!!) :: List n a -> Fin n -> a

findIndex :: Alternative p => (a -> Bool) -> List n a -> p (Fin n)

Find the indices of all elements satisfying the given predicate, gathering them in p.