Stability | experimental |
---|---|
Maintainer | conal@conal.net |
Safe Haskell | Safe-Inferred |
Experiment in length-typed vectors
- module TypeUnary.TyNat
- data Nat where
- zero :: Nat N0
- one :: Nat N1
- two :: Nat N2
- three :: Nat N3
- four :: Nat N4
- withIsNat :: (IsNat n => Nat n -> a) -> Nat n -> a
- natSucc :: Nat n -> Nat (S n)
- natIsNat :: Nat n -> IsNat n => Nat n
- natToZ :: (Enum a, Num a) => Nat n -> a
- natEq :: Nat m -> Nat n -> Maybe (m :=: n)
- natAdd :: Nat m -> Nat n -> Nat (m :+: n)
- natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
- class IsNat n where
- induction :: forall p. p Z -> (forall n. IsNat n => p n -> p (S n)) -> forall n. IsNat n => p n
- data m :<: n where
- succLim :: (m :<: n) -> m :<: S n
- data Index lim = forall n . IsNat n => Index (n :<: lim) (Nat n)
- unIndex :: (Num a, Enum a) => Index m -> a
- succI :: Index m -> Index (S m)
- index0 :: Index (N1 :+: m)
- index1 :: Index (N2 :+: m)
- index2 :: Index (N3 :+: m)
- index3 :: Index (N4 :+: m)
- coerceToIndex :: (Eq i, Show i, Num i, IsNat m) => i -> Index m