TypeNat-0.5.0.0: Some Nat-indexed types for GHC

Safe HaskellNone
LanguageHaskell2010

Data.TypeNat.Fin

Synopsis

Documentation

data Fin :: Nat -> * where Source #

Finite set datatype.

Constructors

FZ :: Fin (S n) 
FS :: Fin k -> Fin (S k) 

ix1 :: Fin (S n) Source #

ix2 :: Fin (S (S n)) Source #

ix3 :: Fin (S (S (S n))) Source #

ix4 :: Fin (S (S (S (S n)))) Source #

ix5 :: Fin (S (S (S (S (S n))))) Source #

ix6 :: Fin (S (S (S (S (S (S n)))))) Source #

ix7 :: Fin (S (S (S (S (S (S (S n))))))) Source #

ix8 :: Fin (S (S (S (S (S (S (S (S n)))))))) Source #

ix9 :: Fin (S (S (S (S (S (S (S (S (S n))))))))) Source #

ix10 :: Fin (S (S (S (S (S (S (S (S (S (S n)))))))))) Source #

safeIndex :: Fin n -> Vect n a -> a Source #

Safely index a Vect.

safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a Source #

Safely update a Vect.