| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Nat
- data Nat
- natPlus :: Nat -> Nat -> Nat
- natMul :: Nat -> Nat -> Nat
- type SNat z = Sing z
- type family a :* a :: Nat
- data (:*$) l
- data l :*$$ l
- type family a :+ a :: Nat
- data (:+$) l
- data l :+$$ l
- data SSym0 l = forall arg . (KindOf (Apply SSym0 arg) ~ KindOf (SSym1 arg)) => SSym0KindInference
- type SSym1 t = S t
- type ZSym0 = Z
- (%:+) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t)
- (%:*) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:*$) t) t)
- type family Lit n
- type SLit n = Sing (Lit n)
Documentation
Instances
| Eq Nat | |
| Ord Nat | |
| Show Nat | |
| SingI Nat Z | |
| POrd Nat (KProxy Nat) | |
| SEq Nat (KProxy Nat) | |
| PEq Nat (KProxy Nat) | |
| SDecide Nat (KProxy Nat) | |
| SingI Nat n0 => SingI Nat (S n) | |
| SingKind Nat (KProxy Nat) | |
| SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:*$$) | |
| SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:+$$) | |
| SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:*$) | |
| SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:+$) | |
| SuppressUnusedWarnings (TyFun Nat Nat -> *) SSym0 | |
| data Sing Nat where | |
| type Compare Nat Z Z = EQ | |
| type (:==) Nat a0 b0 | |
| type Apply Nat Nat SSym0 l0 = SSym1 l0 | |
| type Compare Nat Z (S rhs0) = LT | |
| type Apply Nat Nat ((:*$$) l1) l0 | |
| type Apply Nat Nat ((:+$$) l1) l0 | |
| type DemoteRep Nat (KProxy Nat) = Nat | |
| type Compare Nat (S lhs0) Z = GT | |
| type Compare Nat (S lhs0) (S rhs0) = ThenCmp EQ (Compare Nat lhs0 rhs0) | |
| type Apply (TyFun Nat Nat -> *) Nat (:*$) l0 = (:*$$) l0 | |
| type Apply (TyFun Nat Nat -> *) Nat (:+$) l0 = (:+$$) l0 |
natPlus :: Nat -> Nat -> Nat Source
This is the plain value-level version of addition on Nats. There's rarely a reason to use this; it's included for completeness.
Provides a shorthand for Nat-s using GHC.TypeLits, for example:
>>>:kind! Lit 3Lit 3 :: Nat = 'S ('S ('S 'Z))