Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Fin :: Nat -> * where
- ix1 :: forall (n :: Nat). Fin ('S n)
- ix2 :: forall (n :: Nat). Fin ('S ('S n))
- ix3 :: forall (n :: Nat). Fin ('S ('S ('S n)))
- ix4 :: forall (n :: Nat). Fin ('S ('S ('S ('S n))))
- ix5 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S n)))))
- ix6 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S n))))))
- ix7 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S n)))))))
- ix8 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S ('S n))))))))
- ix9 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S n)))))))))
- ix10 :: forall (n :: Nat). Fin ('S ('S ('S ('S ('S ('S ('S ('S ('S ('S n))))))))))
- safeIndex :: Fin n -> Vect n a -> a
- safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a
- module Data.TypeNat.Nat
Documentation
module Data.TypeNat.Nat