Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- data Nat
- type family NatPlus (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatMul (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatMinus (a :: Nat) (a :: Nat) :: Nat where ...
- type family NatAbs (a :: Nat) :: Nat where ...
- type family NatSignum (a :: Nat) :: Nat where ...
- natPlus :: Nat -> Nat -> Nat
- natMul :: Nat -> Nat -> Nat
- natMinus :: Nat -> Nat -> Nat
- natAbs :: Nat -> Nat
- natSignum :: Nat -> Nat
- someNatVal :: Integer -> Maybe (SomeSing Nat)
- data SNat :: Nat -> Type where
- type family Sing :: k -> Type
- class PNum a
- class SNum a
- data SSym0 :: (~>) Nat Nat where
- type family SSym1 (a6989586621679055807 :: Nat) :: Nat where ...
- type family ZSym0 :: Nat where ...
- type family Lit n where ...
- data LitSym0 :: (~>) Natural Nat where
- type family LitSym1 (a6989586621679112600 :: Natural) :: Nat where ...
- type SLit n = Sing (Lit n)
- sLit :: forall (n :: Nat). SingI (Lit n) => Sing (Lit n)
Documentation
Instances
Num Nat Source # | |
Show Nat Source # | |
Eq Nat Source # | |
Ord Nat Source # | |
SingKind Nat Source # | |
SDecide Nat => SDecide Nat Source # | |
PEq Nat Source # | |
SEq Nat => SEq Nat Source # | |
POrd Nat Source # | |
SOrd Nat => SOrd Nat Source # | |
Defined in Data.Nat sCompare :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) # (%<) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) # (%<=) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) # (%>) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) # (%>=) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) # sMax :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) # sMin :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) # | |
PNum Nat Source # | |
SNum Nat Source # | |
Defined in Data.Nat (%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) # | |
PShow Nat Source # | |
SShow Nat => SShow Nat Source # | |
Defined in Data.Nat sShowsPrec :: forall (t1 :: Natural) (t2 :: Nat) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) # sShow_ :: forall (t :: Nat). Sing t -> Sing (Apply Show_Sym0 t) # sShowList :: forall (t1 :: [Nat]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) # | |
SDecide Nat => TestCoercion SNat Source # | |
SDecide Nat => TestEquality SNat Source # | |
SingI 'Z Source # | |
SingI1 'S Source # | |
SingI n => SingI ('S n :: Nat) Source # | |
SingI SSym0 Source # | |
SuppressUnusedWarnings SSym0 Source # | |
Defined in Data.Nat suppressUnusedWarnings :: () # | |
SuppressUnusedWarnings LitSym0 Source # | |
Defined in Data.Nat suppressUnusedWarnings :: () # | |
type Demote Nat Source # | |
type Sing Source # | |
type Abs (a :: Nat) Source # | |
type FromInteger a Source # | |
Defined in Data.Nat type FromInteger a | |
type Negate (arg :: Nat) Source # | |
type Signum (a :: Nat) Source # | |
type Show_ (arg :: Nat) Source # | |
type (arg :: Nat) /= (arg1 :: Nat) Source # | |
type (a1 :: Nat) == (a2 :: Nat) Source # | |
type (arg :: Nat) < (arg1 :: Nat) Source # | |
type (arg :: Nat) <= (arg1 :: Nat) Source # | |
type (arg :: Nat) > (arg1 :: Nat) Source # | |
type (arg :: Nat) >= (arg1 :: Nat) Source # | |
type Compare (a1 :: Nat) (a2 :: Nat) Source # | |
type Max (arg :: Nat) (arg1 :: Nat) Source # | |
type Min (arg :: Nat) (arg1 :: Nat) Source # | |
type (a1 :: Nat) * (a2 :: Nat) Source # | |
type (a1 :: Nat) + (a2 :: Nat) Source # | |
type (a1 :: Nat) - (a2 :: Nat) Source # | |
type ShowList (arg :: [Nat]) arg1 Source # | |
type Apply SSym0 (a6989586621679055807 :: Nat) Source # | |
type Apply LitSym0 (a6989586621679112600 :: Natural) Source # | |
type ShowsPrec a1 (a2 :: Nat) a3 Source # | |
type family Sing :: k -> Type #
The singleton kind-indexed type family.
Instances
(%+), (%*), sAbs, sSignum, sFromInteger
Instances
SNum Nat Source # | |
Defined in Data.Nat (%+) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%*) :: forall (t1 :: Nat) (t2 :: Nat). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) # sNegate :: forall (t :: Nat). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Nat). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Nat). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) # | |
SNum Natural | |
Defined in GHC.Num.Singletons (%+) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%*) :: forall (t1 :: Natural) (t2 :: Natural). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) # sNegate :: forall (t :: Natural). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Natural). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Natural). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) # | |
SNum a => SNum (Down a) | |
Defined in GHC.Num.Singletons (%+) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%*) :: forall (t1 :: Down a) (t2 :: Down a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) # sNegate :: forall (t :: Down a). Sing t -> Sing (Apply NegateSym0 t) # sAbs :: forall (t :: Down a). Sing t -> Sing (Apply AbsSym0 t) # sSignum :: forall (t :: Down a). Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) # |
type family Lit n where ... Source #
Provides a shorthand for Nat
-s using GHC.TypeLits, for example:
>>>
:kind! Lit 3
Lit 3 :: Nat = 'S ('S ('S 'Z))