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 :: Bool
- zeroCong :: (x ~ y) :- (IsZero x ~ IsZero y)
- zNotS :: (Z ~ S x) :- Fail
- type family NatEq x y :: Bool
- type family Iota x :: [N]
- iotaCong :: (x ~ y) :- (Iota x ~ Iota y)
- type family Pred x :: N
- predCong :: (x ~ y) :- (Pred x ~ Pred y)
- type family x + y :: N
- addCong :: (w ~ y, x ~ z) :- ((w + x) ~ (y + z))
- type family x * y :: N
- mulCong :: (w ~ y, x ~ z) :- ((w * x) ~ (y * z))
- type family x ^ y :: N
- expCong :: (w ~ y, x ~ z) :- ((w ^ x) ~ (y ^ z))
- type family Len as :: N
- lenCong :: (as ~ bs) :- (Len as ~ Len bs)
- type family Ix x as :: k
- ixCong :: (x ~ y, as ~ bs) :- (Ix x as ~ Ix y bs)
- type family x < y :: Bool
- type (<=) x y = (x == y) || (x < y)
- type family x > y :: Bool
- 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' (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) (VT 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 = NatEq x y Source | |
type KnownC N Nat Z = ØC | |
type BoolEqC N Nat a b = ØC | |
type KnownC N Nat (S n) = Known N Nat n Source | |
type WitnessC ØC ((~) N (S n') n) (Fin n) = (~) N n' (Pred n) Source | |
type WitnessC ØC (Known N Nat n) (Nat n) = ØC | |
type WitnessC ØC ((~) N (S x') x) (IFin x y) = (~) N x' (Pred x) Source | |
type WitnessC ØC (Known N Nat n) (VT k n f a) = ØC | |
type WitnessC ØC ((~) N x (S x'), Known N Nat y, (~) Bool lt False, (~) Bool eq False, (~) Bool gt True) (NatGT x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N x' (Pred x)) Source | |
type WitnessC ØC ((~) N x y, Known N Nat x, (~) Bool lt False, (~) Bool eq True, (~) Bool gt False) (NatEQ x y) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) 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) = ((~) Bool lt ((<) x y), (~) Bool eq ((==) N x y), (~) Bool gt ((>) x y), (~) N y' (Pred y)) Source |