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
- type family NatEq x y :: Bool
- type family Iota x :: [N]
- type family Pred x :: N
- type family x + y :: N
- type family x * y :: N
- type family x ^ y :: N
- 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
- type family a == b :: Bool
Documentation
Eq N Source | |
Ord N Source | |
Show N Source | |
TestEquality N Nat | |
DecEquality N Nat Source | |
Known N Nat Z Source | |
Known N Nat n => Known N Nat (S n) Source | If |
(~) 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 |
Witness ØC (Known N Nat n) (VT k n f a) Source | |
type (==) N x y = NatEq x y Source | |
type KnownC N Nat Z = Ø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 (Known N Nat n) (VT k n f a) = ØC |
type family a == b :: Bool infix 4
A type family to compute Boolean equality. Instances are provided
only for open kinds, such as *
and function kinds. Instances are
also provided for datatypes exported from base. A poly-kinded instance
is not provided, as a recursive definition for algebraic kinds is
generally more useful.
type (==) Bool a b = EqBool a b | |
type (==) Ordering a b = EqOrdering a b | |
type (==) * a b = EqStar a b | |
type (==) () a b = EqUnit a b | |
type (==) N x y = NatEq x y | |
type (==) [k] a b = EqList k a b | |
type (==) (Maybe k) a b = EqMaybe k a b | |
type (==) (k -> k1) a b = EqArrow k k1 a b | |
type (==) (Either k k1) a b = EqEither k k1 a b | |
type (==) ((,) k k1) a b = Eq2 k k1 a b | |
type (==) ((,,) k k1 k2) a b = Eq3 k k1 k2 a b | |
type (==) ((,,,) k k1 k2 k3) a b = Eq4 k k1 k2 k3 a b | |
type (==) ((,,,,) k k1 k2 k3 k4) a b = Eq5 k k1 k2 k3 k4 a b | |
type (==) ((,,,,,) k k1 k2 k3 k4 k5) a b = Eq6 k k1 k2 k3 k4 k5 a b | |
type (==) ((,,,,,,) k k1 k2 k3 k4 k5 k6) a b = Eq7 k k1 k2 k3 k4 k5 k6 a b | |
type (==) ((,,,,,,,) k k1 k2 k3 k4 k5 k6 k7) a b = Eq8 k k1 k2 k3 k4 k5 k6 k7 a b | |
type (==) ((,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8) a b = Eq9 k k1 k2 k3 k4 k5 k6 k7 k8 a b | |
type (==) ((,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9) a b = Eq10 k k1 k2 k3 k4 k5 k6 k7 k8 k9 a b | |
type (==) ((,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10) a b = Eq11 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 a b | |
type (==) ((,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11) a b = Eq12 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 a b | |
type (==) ((,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12) a b = Eq13 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 a b | |
type (==) ((,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13) a b = Eq14 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 a b | |
type (==) ((,,,,,,,,,,,,,,) k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14) a b = Eq15 k k1 k2 k3 k4 k5 k6 k7 k8 k9 k10 k11 k12 k13 k14 a b |