TypeNat-0.2.1.0: Some Nat-indexed types for GHC

Safe HaskellSafe-Inferred
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 :: Vect a n -> Fin n -> a Source

Safely index a Vect.

module Data.TypeNat.Nat