Copyright | Copyright (C) 2015 Kyle Carter |
---|---|
License | BSD3 |
Maintainer | Kyle Carter <kylcarte@indiana.edu> |
Stability | experimental |
Portability | RankNTypes |
Safe Haskell | None |
Language | Haskell2010 |
Type-level natural numbers, along with frequently used type families over them.
- data N
- fromInt :: Int -> Maybe N
- type family IsZero (x :: N) :: Bool where ...
- zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)
- zNotS :: (Z ~ S x) :- Fail
- type family NatEq (x :: N) (y :: N) :: Bool where ...
- type family Iota (x :: N) = (xs :: [N]) | xs -> x where ...
- iotaCong :: (x ~ y) :- (Iota x ~ Iota y)
- type family Pred (x :: N) :: N where ...
- type Pos n = n ~ S (Pred n)
- predCong :: (x ~ y) :- (Pred x ~ Pred y)
- type family (x :: N) + (y :: N) :: N where ...
- data AddW f :: N -> * where
- addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))
- type family (x :: N) * (y :: N) :: N where ...
- data MulW f :: N -> * where
- mulCong :: (w ~ y, x ~ z) :- ((w * x) ~ (y * z))
- type family (x :: N) ^ (y :: N) :: N where ...
- expCong :: (w ~ y, x ~ z) :- ((w ^ x) ~ (y ^ z))
- type family Len (as :: [k]) :: N where ...
- lenCong :: (as ~ bs) :- (Len as ~ Len bs)
- type family Ix (x :: N) (as :: [k]) :: k where ...
- ixCong :: (x ~ y, as ~ bs) :- (Ix x as ~ Ix y bs)
- type family (x :: N) < (y :: N) :: Bool where ...
- type (<=) x y = (x == y) || (x < y)
- type family (x :: N) > (y :: N) :: Bool where ...
- type (>=) x y = (x == y) || (x > y)
- type N0 = Z
- type N1 = S N0
- type N2 = S N1
- type N3 = S N2
- type N4 = S N3
- type N5 = S N4
- type N6 = S N5
- type N7 = S N6
- type N8 = S N7
- type N9 = S N8
- type N10 = S N9
Documentation
Eq N Source # | |
Ord N Source # | |
Show N Source # | |
TestEquality N Nat # | |
Read1 N Nat Source # | |
Read1 N Fin Source # | |
Show1 N Nat Source # | |
Show1 N Fin Source # | |
Ord1 N Nat Source # | |
Ord1 N Fin Source # | |
Eq1 N Nat Source # | |
Eq1 N Fin Source # | |
BoolEquality N Nat Source # | |
Known N Nat Z Source # | |
Read2 N N IFin Source # | |
Show2 N N IFin Source # | |
Ord2 N N IFin Source # | |
Eq2 N N IFin Source # | |
Known N Nat n => Known N Nat (S n) Source # | If |
Show1 N (IFin x) Source # | |
Ord1 N (IFin x) Source # | |
Eq1 N (IFin x) Source # | |
(~) N n (Len k as) => Witness ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
(~) N n' (Pred n) => Witness ØC ((~) N (S n') n) (Fin n) Source # | A That is, |
Witness ØC (Known N Nat n) (Nat n) Source # | A |
(~) N x' (Pred x) => Witness ØC ((~) N (S x') x) (IFin x y) Source # | An That is, |
Witness ØC (Known N Nat n) (VecT k n f a) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) => Witness ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y)) => Witness ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source # | |
((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) => Witness ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source # | |
type (==) N x y Source # | |
type KnownC N Nat Z Source # | |
type KnownC N Nat (S n) Source # | |
type WitnessC ØC (Known N Nat n, Known [k] (Length k) as) (Length k as) Source # | |
type WitnessC ØC ((~) N (S n') n) (Fin n) Source # | |
type WitnessC ØC (Known N Nat n) (Nat n) Source # | |
type WitnessC ØC ((~) N (S x') x) (IFin x y) Source # | |
type WitnessC ØC (Known N Nat n) (VecT k n f a) Source # | |
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) Source # | |
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) Source # | |
type WitnessC ØC ((~) N y (S y'), Known N Nat x, (~) Bool lt True, (~) Bool eq False, (~) Bool gt False) (NatLT x y) Source # | |