Data.TypeNat.Fin

Documentation

data Fin :: Nat -> * where

Finite set datatype.

Constructors

FZ :: Fin (S n)

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

ix1 :: Fin (S n)

ix2 :: Fin (S (S n))

ix3 :: Fin (S (S (S n)))

ix4 :: Fin (S (S (S (S n))))

ix5 :: Fin (S (S (S (S (S n)))))

ix6 :: Fin (S (S (S (S (S (S n))))))

ix7 :: Fin (S (S (S (S (S (S (S n)))))))

ix8 :: Fin (S (S (S (S (S (S (S (S n))))))))

ix9 :: Fin (S (S (S (S (S (S (S (S (S n)))))))))

ix10 :: Fin (S (S (S (S (S (S (S (S (S (S n))))))))))

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

Safely index a Vect.

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

Safely update a Vect.

module Data.TypeNat.Nat