Safe Haskell	None
Language	Haskell2010

Data.Type.Natural.Class.Arithmetic

Synopsis

type family Zero nat :: nat where ...
type family One nat :: nat where ...
type S n = Succ n
sZero :: SNum nat => Sing (Zero nat)
sOne :: SNum nat => Sing (One nat)
data ZeroOrSucc (n :: nat) where
- IsZero :: ZeroOrSucc (Zero nat)
- IsSucc :: Sing n -> ZeroOrSucc (Succ n)
plusCong :: (n :~: m) -> (n' :~: m') -> (n + n') :~: (m + m')
plusCongR :: Sing k -> (n :~: m) -> (k + n) :~: (k + m)
plusCongL :: (n :~: m) -> Sing k -> (n + k) :~: (m + k)
succCong :: (n :~: m) -> S n :~: S m
multCong :: (n :~: m) -> (l :~: k) -> (n * l) :~: (m * k)
multCongL :: (n :~: m) -> Sing k -> (n * k) :~: (m * k)
multCongR :: Sing k -> (n :~: m) -> (k * n) :~: (k * m)
minusCong :: (n :~: m) -> (l :~: k) -> (n - l) :~: (m - k)
minusCongL :: (n :~: m) -> Sing k -> (n - k) :~: (m - k)
minusCongR :: Sing k -> (n :~: m) -> (k - n) :~: (k - m)
class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where
pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n
pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n
type (+@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t + t1
data (l :: a6989586621679412326) +@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *
data (+@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *
type (-@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t - t1
data (l :: a6989586621679412326) -@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *
data (-@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *
type (*@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t * t1
data (l :: a6989586621679412326) *@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *
data (*@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *
type FromIntegerSym1 (t :: Nat) = (FromInteger t :: k)
data FromIntegerSym0 (l :: TyFun Nat a6989586621679412326) :: forall a6989586621679412326. TyFun Nat a6989586621679412326 -> *
class PNum a where
- type (arg :: a) + (arg1 :: a) :: a
- type (arg :: a) - (arg1 :: a) :: a
- type (arg :: a) * (arg1 :: a) :: a
- type Negate (arg :: a) :: a
- type Abs (arg :: a) :: a
- type Signum (arg :: a) :: a
- type FromInteger (arg :: Nat) :: a
class SNum a where
type (==@#@$$$) (t :: a6989586621679288106) (t1 :: a6989586621679288106) = t == t1
data (l :: a6989586621679288106) ==@#@$$ (l1 :: TyFun a6989586621679288106 Bool) :: forall a6989586621679288106. a6989586621679288106 -> TyFun a6989586621679288106 Bool -> *
data (==@#@$) (l :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type)) :: forall a6989586621679288106. TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *
type (/=@#@$$$) (t :: a6989586621679288106) (t1 :: a6989586621679288106) = t /= t1
data (l :: a6989586621679288106) /=@#@$$ (l1 :: TyFun a6989586621679288106 Bool) :: forall a6989586621679288106. a6989586621679288106 -> TyFun a6989586621679288106 Bool -> *
data (/=@#@$) (l :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type)) :: forall a6989586621679288106. TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *
(%==) :: SEq k => Sing a -> Sing b -> Sing (a == b)
(%/=) :: SEq k => Sing a -> Sing b -> Sing (a /= b)
type family (x :: a) == (y :: a) :: Bool
type family (x :: a) /= (y :: a) :: Bool

Documentation

type family Zero nat :: nat where ... Source #

Equations

Zero nat = FromInteger 0

type family One nat :: nat where ... Source #

Equations

One nat = FromInteger 1

type S n = Succ n Source #

sZero :: SNum nat => Sing (Zero nat) Source #

sOne :: SNum nat => Sing (One nat) Source #

data ZeroOrSucc (n :: nat) where Source #

Constructors

IsZero :: ZeroOrSucc (Zero nat)
IsSucc :: Sing n -> ZeroOrSucc (Succ n)

plusCong :: (n :~: m) -> (n' :~: m') -> (n + n') :~: (m + m') Source #

plusCongR :: Sing k -> (n :~: m) -> (k + n) :~: (k + m) Source #

plusCongL :: (n :~: m) -> Sing k -> (n + k) :~: (m + k) Source #

succCong :: (n :~: m) -> S n :~: S m Source #

multCong :: (n :~: m) -> (l :~: k) -> (n * l) :~: (m * k) Source #

multCongL :: (n :~: m) -> Sing k -> (n * k) :~: (m * k) Source #

multCongR :: Sing k -> (n :~: m) -> (k * n) :~: (k * m) Source #

minusCong :: (n :~: m) -> (l :~: k) -> (n - l) :~: (m - k) Source #

minusCongL :: (n :~: m) -> Sing k -> (n - k) :~: (m - k) Source #

minusCongR :: Sing k -> (n :~: m) -> (k - n) :~: (k - m) Source #

class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind nat) => IsPeano nat where Source #

Minimal complete definition

succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction

Methods

succOneCong :: Succ (Zero nat) :~: One nat Source #

succInj :: (Succ n :~: Succ (m :: nat)) -> n :~: m Source #

succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ (m :: nat)) -> n :~: m Source #

succNonCyclic :: Sing n -> (Succ n :~: Zero nat) -> Void Source #

induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k Source #

plusMinus :: Sing (n :: nat) -> Sing m -> ((n + m) - m) :~: n Source #

plusMinus' :: Sing (n :: nat) -> Sing m -> ((n + m) - n) :~: m Source #

plusZeroL :: Sing n -> (Zero nat + n) :~: n Source #

plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m :: nat) Source #

plusZeroR :: Sing n -> (n + Zero nat) :~: n Source #

plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m :: nat) Source #

plusComm :: Sing n -> Sing m -> (n + m) :~: ((m :: nat) + n) Source #

plusAssoc :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l)) Source #

multZeroL :: Sing n -> (Zero nat * n) :~: Zero nat Source #

multSuccL :: Sing (n :: nat) -> Sing m -> (S n * m) :~: ((n * m) + m) Source #

multZeroR :: Sing n -> (n * Zero nat) :~: Zero nat Source #

multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + (n :: nat)) Source #

multComm :: Sing (n :: nat) -> Sing m -> (n * m) :~: (m * n) Source #

multOneR :: Sing n -> (n * One nat) :~: n Source #

multOneL :: Sing n -> (One nat * n) :~: n Source #

plusMultDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l)) Source #

multPlusDistrib :: Sing (n :: nat) -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l)) Source #

minusNilpotent :: Sing n -> (n - n) :~: Zero nat Source #

multAssoc :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l)) Source #

plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l Source #

plusEqCancelR :: forall n m l. Sing (n :: nat) -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m Source #

succAndPlusOneL :: Sing n -> Succ n :~: (One nat + n) Source #

succAndPlusOneR :: Sing n -> Succ n :~: (n + One nat) Source #

predSucc :: Sing n -> Pred (Succ n) :~: (n :: nat) Source #

zeroOrSucc :: Sing (n :: nat) -> ZeroOrSucc n Source #

plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> n :~: Zero nat Source #

plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero nat) -> m :~: Zero nat Source #

predUnique :: Sing (n :: nat) -> Sing m -> (Succ n :~: m) -> n :~: Pred m Source #

multEqSuccElimL :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n) Source #

multEqSuccElimR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m) Source #

minusZero :: Sing n -> (n - Zero nat) :~: n Source #

multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m Source #

succPred :: Sing n -> ((n :~: Zero nat) -> Void) -> Succ (Pred n) :~: n Source #

multEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l Source #

sPred' :: proxy n -> Sing (Succ n) -> Sing (n :: nat) Source #

toNatural :: Sing (n :: nat) -> Natural Source #

fromNatural :: Natural -> SomeSing nat Source #

Instances

IsPeano Nat Source #
Instance details Defined in Data.Type.Natural.Builtin Methods succOneCong :: Succ (Zero Nat) :~: One Nat Source # succInj :: (Succ n :~: Succ m) -> n :~: m Source # succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m Source # succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void Source # induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k Source # plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n Source # plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m Source # plusZeroL :: Sing n -> (Zero Nat + n) :~: n Source # plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m) Source # plusZeroR :: Sing n -> (n + Zero Nat) :~: n Source # plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m) Source # plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n) Source # plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l)) Source # multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat Source # multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m) Source # multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat Source # multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n) Source # multComm :: Sing n -> Sing m -> (n * m) :~: (m * n) Source # multOneR :: Sing n -> (n * One Nat) :~: n Source # multOneL :: Sing n -> (One Nat * n) :~: n Source # plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l)) Source # multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l)) Source # minusNilpotent :: Sing n -> (n - n) :~: Zero Nat Source # multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l)) Source # plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l Source # plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m Source # succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n) Source # succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat) Source # predSucc :: Sing n -> Pred (Succ n) :~: n Source # zeroOrSucc :: Sing n -> ZeroOrSucc n Source # plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat Source # plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat Source # predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m Source # multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n) Source # multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m) Source # minusZero :: Sing n -> (n - Zero Nat) :~: n Source # multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m Source # succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n Source # multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l Source # sPred' :: proxy n -> Sing (Succ n) -> Sing n Source # toNatural :: Sing n -> Natural Source # fromNatural :: Natural -> SomeSing Nat Source #
IsPeano Nat Source #	Since 0.5.0.0
Instance details Defined in Data.Type.Natural Methods succOneCong :: Succ (Zero Nat) :~: One Nat Source # succInj :: (Succ n :~: Succ m) -> n :~: m Source # succInj' :: proxy n -> proxy' m -> (Succ n :~: Succ m) -> n :~: m Source # succNonCyclic :: Sing n -> (Succ n :~: Zero Nat) -> Void Source # induction :: p (Zero Nat) -> (forall (n :: Nat). Sing n -> p n -> p (S n)) -> Sing k -> p k Source # plusMinus :: Sing n -> Sing m -> ((n + m) - m) :~: n Source # plusMinus' :: Sing n -> Sing m -> ((n + m) - n) :~: m Source # plusZeroL :: Sing n -> (Zero Nat + n) :~: n Source # plusSuccL :: Sing n -> Sing m -> (S n + m) :~: S (n + m) Source # plusZeroR :: Sing n -> (n + Zero Nat) :~: n Source # plusSuccR :: Sing n -> Sing m -> (n + S m) :~: S (n + m) Source # plusComm :: Sing n -> Sing m -> (n + m) :~: (m + n) Source # plusAssoc :: Sing n -> Sing m -> Sing l -> ((n + m) + l) :~: (n + (m + l)) Source # multZeroL :: Sing n -> (Zero Nat * n) :~: Zero Nat Source # multSuccL :: Sing n -> Sing m -> (S n * m) :~: ((n * m) + m) Source # multZeroR :: Sing n -> (n * Zero Nat) :~: Zero Nat Source # multSuccR :: Sing n -> Sing m -> (n * S m) :~: ((n * m) + n) Source # multComm :: Sing n -> Sing m -> (n * m) :~: (m * n) Source # multOneR :: Sing n -> (n * One Nat) :~: n Source # multOneL :: Sing n -> (One Nat * n) :~: n Source # plusMultDistrib :: Sing n -> Sing m -> Sing l -> ((n + m) * l) :~: ((n * l) + (m * l)) Source # multPlusDistrib :: Sing n -> Sing m -> Sing l -> (n * (m + l)) :~: ((n * m) + (n * l)) Source # minusNilpotent :: Sing n -> (n - n) :~: Zero Nat Source # multAssoc :: Sing n -> Sing m -> Sing l -> ((n * m) * l) :~: (n * (m * l)) Source # plusEqCancelL :: Sing n -> Sing m -> Sing l -> ((n + m) :~: (n + l)) -> m :~: l Source # plusEqCancelR :: Sing n -> Sing m -> Sing l -> ((n + l) :~: (m + l)) -> n :~: m Source # succAndPlusOneL :: Sing n -> Succ n :~: (One Nat + n) Source # succAndPlusOneR :: Sing n -> Succ n :~: (n + One Nat) Source # predSucc :: Sing n -> Pred (Succ n) :~: n Source # zeroOrSucc :: Sing n -> ZeroOrSucc n Source # plusEqZeroL :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> n :~: Zero Nat Source # plusEqZeroR :: Sing n -> Sing m -> ((n + m) :~: Zero Nat) -> m :~: Zero Nat Source # predUnique :: Sing n -> Sing m -> (Succ n :~: m) -> n :~: Pred m Source # multEqSuccElimL :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> n :~: Succ (Pred n) Source # multEqSuccElimR :: Sing n -> Sing m -> Sing l -> ((n * m) :~: Succ l) -> m :~: Succ (Pred m) Source # minusZero :: Sing n -> (n - Zero Nat) :~: n Source # multEqCancelR :: Sing n -> Sing m -> Sing l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m Source # succPred :: Sing n -> ((n :~: Zero Nat) -> Void) -> Succ (Pred n) :~: n Source # multEqCancelL :: Sing n -> Sing m -> Sing l -> ((Succ n * m) :~: (Succ n * l)) -> m :~: l Source # sPred' :: proxy n -> Sing (Succ n) -> Sing n Source # toNatural :: Sing n -> Natural Source # fromNatural :: Natural -> SomeSing Nat Source #

pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n Source #

pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n Source #

type (+@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t + t1 #

data (l :: a6989586621679412326) +@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> * #

Instances

SuppressUnusedWarnings ((+@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 + l2

data (+@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> * #

Instances

SuppressUnusedWarnings ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((+@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326) = (+@#@$$) l

type (-@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t - t1 #

data (l :: a6989586621679412326) -@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> * #

Instances

SuppressUnusedWarnings ((-@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> *)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$$) l1 :: TyFun a a -> *) (l2 :: a) = l1 - l2

data (-@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> * #

Instances

SuppressUnusedWarnings ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((-@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> *) (l :: a6989586621679412326) = (-@#@$$) l

type (*@#@$$$) (t :: a6989586621679412326) (t1 :: a6989586621679412326) = t * t1 #

data (l :: a6989586621679412326) *@#@$$ (l1 :: TyFun a6989586621679412326 a6989586621679412326) :: forall a6989586621679412326. a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> * #

Instances

SuppressUnusedWarnings ((@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> )
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2

data (*@#@$) (l :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type)) :: forall a6989586621679412326. TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> * #

Instances

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> )
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> ) (l :: a6989586621679412326)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> ) (l :: a6989586621679412326) = (*@#@$$) l

type FromIntegerSym1 (t :: Nat) = (FromInteger t :: k) #

data FromIntegerSym0 (l :: TyFun Nat a6989586621679412326) :: forall a6989586621679412326. TyFun Nat a6989586621679412326 -> * #

Instances

SuppressUnusedWarnings (FromIntegerSym0 :: TyFun Nat a6989586621679412326 -> *)
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat)
Instance details Defined in Data.Singletons.Prelude.Num type Apply (FromIntegerSym0 :: TyFun Nat k2 -> *) (l :: Nat) = (FromInteger l :: k2)

class PNum a #

Associated Types

type (arg :: a) + (arg1 :: a) :: a #

type (arg :: a) - (arg1 :: a) :: a #

type (arg :: a) * (arg1 :: a) :: a #

type Negate (arg :: a) :: a #

type Abs (arg :: a) :: a #

type Signum (arg :: a) :: a #

type FromInteger (arg :: Nat) :: a #

Instances

PNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #
PNum Nat #
Instance details Defined in Data.Type.Natural.Definitions Associated Types type arg + arg1 :: a # type arg - arg1 :: a # type arg * arg1 :: a # type Negate arg :: a # type Abs arg :: a # type Signum arg :: a # type FromInteger arg :: a #

class SNum a where #

Minimal complete definition

(%+), (%*), sAbs, sSignum, sFromInteger

Methods

(%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((+@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 6 #

(%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((-@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 6 #

(%*) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply ((*@#@$) :: TyFun a (TyFun a a -> Type) -> *) t1) t2) infixl 7 #

sNegate :: Sing t -> Sing (Apply (NegateSym0 :: TyFun a a -> *) t) #

sAbs :: Sing t -> Sing (Apply (AbsSym0 :: TyFun a a -> *) t) #

sSignum :: Sing t -> Sing (Apply (SignumSym0 :: TyFun a a -> *) t) #

sFromInteger :: Sing t -> Sing (Apply (FromIntegerSym0 :: TyFun Nat a -> *) t) #

Instances

SNum Nat
Instance details Defined in Data.Singletons.Prelude.Num Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #
SNum Nat #
Instance details Defined in Data.Type.Natural.Definitions Methods (%+) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) # (%-) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) # (%) :: Sing t1 -> Sing t2 -> Sing (Apply (Apply (@#@$) t1) t2) # sNegate :: Sing t -> Sing (Apply NegateSym0 t) # sAbs :: Sing t -> Sing (Apply AbsSym0 t) # sSignum :: Sing t -> Sing (Apply SignumSym0 t) # sFromInteger :: Sing t -> Sing (Apply FromIntegerSym0 t) #

type (==@#@$$$) (t :: a6989586621679288106) (t1 :: a6989586621679288106) = t == t1 #

data (l :: a6989586621679288106) ==@#@$$ (l1 :: TyFun a6989586621679288106 Bool) :: forall a6989586621679288106. a6989586621679288106 -> TyFun a6989586621679288106 Bool -> * #

Instances

SuppressUnusedWarnings ((==@#@$$) :: a6989586621679288106 -> TyFun a6989586621679288106 Bool -> *)
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((==@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 == l2

data (==@#@$) (l :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type)) :: forall a6989586621679288106. TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> * #

Instances

SuppressUnusedWarnings ((==@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *)
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () #
type Apply ((==@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *) (l :: a6989586621679288106)
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((==@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *) (l :: a6989586621679288106) = (==@#@$$) l

type (/=@#@$$$) (t :: a6989586621679288106) (t1 :: a6989586621679288106) = t /= t1 #

data (l :: a6989586621679288106) /=@#@$$ (l1 :: TyFun a6989586621679288106 Bool) :: forall a6989586621679288106. a6989586621679288106 -> TyFun a6989586621679288106 Bool -> * #

Instances

SuppressUnusedWarnings ((/=@#@$$) :: a6989586621679288106 -> TyFun a6989586621679288106 Bool -> *)
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((/=@#@$$) l1 :: TyFun a Bool -> *) (l2 :: a) = l1 /= l2

data (/=@#@$) (l :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type)) :: forall a6989586621679288106. TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> * #

Instances

SuppressUnusedWarnings ((/=@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *)
Instance details Defined in Data.Singletons.Prelude.Eq Methods suppressUnusedWarnings :: () #
type Apply ((/=@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *) (l :: a6989586621679288106)
Instance details Defined in Data.Singletons.Prelude.Eq type Apply ((/=@#@$) :: TyFun a6989586621679288106 (TyFun a6989586621679288106 Bool -> Type) -> *) (l :: a6989586621679288106) = (/=@#@$$) l

(%==) :: SEq k => Sing a -> Sing b -> Sing (a == b) infix 4 #

Boolean equality on singletons

(%/=) :: SEq k => Sing a -> Sing b -> Sing (a /= b) infix 4 #

Boolean disequality on singletons

type family (x :: a) == (y :: a) :: Bool infix 4 #

Instances

type (a :: Bool) == (b :: Bool)
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: Bool) == (b :: Bool) = Equals_6989586621679288995 a b
type (a :: Ordering) == (b :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: Ordering) == (b :: Ordering) = Equals_6989586621679288999 a b
type (a :: Nat) == (b :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (a :: Nat) == (b :: Nat) = a == b
type (a :: Symbol) == (b :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal type (a :: Symbol) == (b :: Symbol) = a == b
type (a :: ()) == (b :: ())
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: ()) == (b :: ()) = Equals_6989586621679289003 a b
type (a :: Nat) == (b :: Nat) #
Instance details Defined in Data.Type.Natural.Definitions type (a :: Nat) == (b :: Nat)
type (a :: Void) == (b :: Void)
Instance details Defined in Data.Singletons.Prelude.Eq type (a :: Void) == (b :: Void) = Equals_6989586621679288778 a b
type (a2 :: [a1]) == (b :: [a1])
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: [a1]) == (b :: [a1]) = Equals_6989586621679288724 a2 b
type (a2 :: Maybe a1) == (b :: Maybe a1)
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: Maybe a1) == (b :: Maybe a1) = Equals_6989586621679288711 a2 b
type (a2 :: NonEmpty a1) == (b :: NonEmpty a1)
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: NonEmpty a1) == (b :: NonEmpty a1) = Equals_6989586621679288763 a2 b
type (a2 :: Either a1 b1) == (b2 :: Either a1 b1)
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: Either a1 b1) == (b2 :: Either a1 b1) = Equals_6989586621679288744 a2 b2
type (a2 :: (a1, b1)) == (b2 :: (a1, b1))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1)) == (b2 :: (a1, b1)) = Equals_6989586621679288784 a2 b2
type (a2 :: (a1, b1, c)) == (b2 :: (a1, b1, c))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1, c)) == (b2 :: (a1, b1, c)) = Equals_6989586621679288803 a2 b2
type (a2 :: (a1, b1, c, d)) == (b2 :: (a1, b1, c, d))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1, c, d)) == (b2 :: (a1, b1, c, d)) = Equals_6989586621679288829 a2 b2
type (a2 :: (a1, b1, c, d, e)) == (b2 :: (a1, b1, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1, c, d, e)) == (b2 :: (a1, b1, c, d, e)) = Equals_6989586621679288862 a2 b2
type (a2 :: (a1, b1, c, d, e, f)) == (b2 :: (a1, b1, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1, c, d, e, f)) == (b2 :: (a1, b1, c, d, e, f)) = Equals_6989586621679288902 a2 b2
type (a2 :: (a1, b1, c, d, e, f, g)) == (b2 :: (a1, b1, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Eq type (a2 :: (a1, b1, c, d, e, f, g)) == (b2 :: (a1, b1, c, d, e, f, g)) = Equals_6989586621679288949 a2 b2

type family (x :: a) /= (y :: a) :: Bool infix 4 #

Instances

type (x :: Bool) /= (y :: Bool)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Bool) /= (y :: Bool) = Not (x == y)
type (x :: Ordering) /= (y :: Ordering)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Ordering) /= (y :: Ordering) = Not (x == y)
type (x :: Nat) /= (y :: Nat)
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (x :: Symbol) /= (y :: Symbol)
Instance details Defined in Data.Singletons.TypeLits.Internal type (x :: Symbol) /= (y :: Symbol) = Not (x == y)
type (x :: ()) /= (y :: ())
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: ()) /= (y :: ()) = Not (x == y)
type (x :: Nat) /= (y :: Nat) #
Instance details Defined in Data.Type.Natural.Definitions type (x :: Nat) /= (y :: Nat) = Not (x == y)
type (x :: Void) /= (y :: Void)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Void) /= (y :: Void) = Not (x == y)
type (x :: [a]) /= (y :: [a])
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: [a]) /= (y :: [a]) = Not (x == y)
type (x :: Maybe a) /= (y :: Maybe a)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Maybe a) /= (y :: Maybe a) = Not (x == y)
type (x :: NonEmpty a) /= (y :: NonEmpty a)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: NonEmpty a) /= (y :: NonEmpty a) = Not (x == y)
type (x :: Either a b) /= (y :: Either a b)
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: Either a b) /= (y :: Either a b) = Not (x == y)
type (x :: (a, b)) /= (y :: (a, b))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b)) /= (y :: (a, b)) = Not (x == y)
type (x :: (a, b, c)) /= (y :: (a, b, c))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b, c)) /= (y :: (a, b, c)) = Not (x == y)
type (x :: (a, b, c, d)) /= (y :: (a, b, c, d))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b, c, d)) /= (y :: (a, b, c, d)) = Not (x == y)
type (x :: (a, b, c, d, e)) /= (y :: (a, b, c, d, e))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b, c, d, e)) /= (y :: (a, b, c, d, e)) = Not (x == y)
type (x :: (a, b, c, d, e, f)) /= (y :: (a, b, c, d, e, f))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b, c, d, e, f)) /= (y :: (a, b, c, d, e, f)) = Not (x == y)
type (x :: (a, b, c, d, e, f, g)) /= (y :: (a, b, c, d, e, f, g))
Instance details Defined in Data.Singletons.Prelude.Eq type (x :: (a, b, c, d, e, f, g)) /= (y :: (a, b, c, d, e, f, g)) = Not (x == y)

SuppressUnusedWarnings ((@#@$$) :: a6989586621679412326 -> TyFun a6989586621679412326 a6989586621679412326 -> )
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$$) l1 :: TyFun a a -> ) (l2 :: a) = l1 * l2

SuppressUnusedWarnings ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> )
Instance details Defined in Data.Singletons.Prelude.Num Methods suppressUnusedWarnings :: () #
type Apply ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> ) (l :: a6989586621679412326)
Instance details Defined in Data.Singletons.Prelude.Num type Apply ((@#@$) :: TyFun a6989586621679412326 (TyFun a6989586621679412326 a6989586621679412326 -> Type) -> ) (l :: a6989586621679412326) = (*@#@$$) l