Data.Fin

Documentation

data Fin :: Peano -> * where

Constructors

Zero :: Fin (Succ n)

Succ :: Fin n -> Fin (Succ n)

Instances

Natural n => Bounded (Fin (Succ n))

Defined in Data.Fin.Private

Methods

minBound :: Fin (Succ n)

maxBound :: Fin (Succ n)

Natural n => Enum (Fin n)

Defined in Data.Fin.Private

Methods

succ :: Fin n -> Fin n

pred :: Fin n -> Fin n

toEnum :: Int -> Fin n

fromEnum :: Fin n -> Int

enumFrom :: Fin n -> [Fin n]

enumFromThen :: Fin n -> Fin n -> [Fin n]

enumFromTo :: Fin n -> Fin n -> [Fin n]

enumFromThenTo :: Fin n -> Fin n -> Fin n -> [Fin n]

Eq (Fin n)

Defined in Data.Fin.Private

Methods

(==) :: Fin n -> Fin n -> Bool

(/=) :: Fin n -> Fin n -> Bool

Natural n => Num (Fin n)

Defined in Data.Fin.Private

Methods

(+) :: Fin n -> Fin n -> Fin n

(-) :: Fin n -> Fin n -> Fin n

(*) :: Fin n -> Fin n -> Fin n

negate :: Fin n -> Fin n

abs :: Fin n -> Fin n

signum :: Fin n -> Fin n

fromInteger :: Integer -> Fin n

Ord (Fin n)

Defined in Data.Fin.Private

Methods

compare :: Fin n -> Fin n -> Ordering

(<) :: Fin n -> Fin n -> Bool

(<=) :: Fin n -> Fin n -> Bool

(>) :: Fin n -> Fin n -> Bool

(>=) :: Fin n -> Fin n -> Bool

max :: Fin n -> Fin n -> Fin n

min :: Fin n -> Fin n -> Fin n

(Natural n, Read (Fin n)) => Read (Fin (Succ n))

Defined in Data.Fin.Private

Methods

readsPrec :: Int -> ReadS (Fin (Succ n))

readList :: ReadS [Fin (Succ n)]

readPrec :: ReadPrec (Fin (Succ n))

readListPrec :: ReadPrec [Fin (Succ n)]

Read (Fin Zero)

Defined in Data.Fin.Private

Methods

readsPrec :: Int -> ReadS (Fin Zero)

readList :: ReadS [Fin Zero]

readPrec :: ReadPrec (Fin Zero)

readListPrec :: ReadPrec [Fin Zero]

Show (Fin n)

Defined in Data.Fin.Private

Methods

showsPrec :: Int -> Fin n -> ShowS

show :: Fin n -> String

showList :: [Fin n] -> ShowS

enum :: Natural n => List n (Fin n)

inj₁ :: Fin n -> Fin (Succ n)

proj₁ :: Natural n => Fin (Succ n) -> Maybe (Fin n)

lift₁ :: (Fin m -> Fin n) -> Fin (Succ m) -> Fin (Succ n)

fromFin :: Integral a => Fin n -> a

toFin :: forall n a. (Natural n, Integral a) => a -> Fin (Succ n)

toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin n)