Fin-0.2.5.1: Finite totally-ordered sets
Data.Fin
data Fin :: Peano -> * where Source #
Constructors
Defined in Data.Fin.Private
Methods
minBound :: Fin (Succ n) #
maxBound :: Fin (Succ n) #
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] #
(==) :: Fin n -> Fin n -> Bool #
(/=) :: Fin n -> Fin n -> Bool #
(+) :: 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 #
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 #
readsPrec :: Int -> ReadS (Fin (Succ n)) #
readList :: ReadS [Fin (Succ n)] #
readPrec :: ReadPrec (Fin (Succ n)) #
readListPrec :: ReadPrec [Fin (Succ n)] #
readsPrec :: Int -> ReadS (Fin Zero) #
readList :: ReadS [Fin Zero] #
readPrec :: ReadPrec (Fin Zero) #
readListPrec :: ReadPrec [Fin Zero] #
showsPrec :: Int -> Fin n -> ShowS #
show :: Fin n -> String #
showList :: [Fin n] -> ShowS #
enum :: Natural n => List n (Fin n) Source #
inj₁ :: Fin n -> Fin (Succ n) Source #
lift₁ :: (Fin m -> Fin n) -> Fin (Succ m) -> Fin (Succ n) Source #
fromFin :: Integral a => Fin n -> a Source #
toFin :: forall n a. (Natural n, Integral a) => a -> Fin (Succ n) Source #
toFinMay :: (Natural n, Integral a) => a -> Maybe (Fin n) Source #