Stability | experimental |
---|---|
Maintainer | conal@conal.net |
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 :: Nat n -> Integer
- natEq :: Nat m -> Nat n -> Maybe (m :=: n)
- natAdd :: Nat m -> Nat n -> Nat (m :+: n)
- class IsNat n where
- data m :<: n where
- data Index lim = forall n . IsNat n => Index (n :<: lim) (Nat n)
- succI :: Index m -> Index (S m)
- index0 :: Index (N1 :+: m)
- index1 :: Index (N2 :+: m)
- index2 :: Index (N3 :+: m)
- index3 :: Index (N4 :+: m)
- coerceToIndex :: (Integral i, IsNat m) => i -> Index m
Documentation
module TypeUnary.TyNat
Value-typed natural numbers
Is n
a natural number type?
Inequality proofs and indices
A number under the given limit, with proof
coerceToIndex :: (Integral i, IsNat m) => i -> Index mSource
Index generation from integer. Can fail dynamically if the integer is too large.