Data.Type.Natural.Class.Arithmetic

Documentation

type family Zero nat :: nat where ...

Equations

Zero nat = FromInteger 0

type family One nat :: nat where ...

Equations

One nat = FromInteger 1

type S n = Succ n

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

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

data ZeroOrSucc (n :: nat) where

Constructors

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

Minimal complete definition

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

Methods

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

fromNatural :: Natural -> SomeSing nat

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

module Data.Singletons.Prelude.Eq

module Data.Singletons.Prelude.Num

module Data.Singletons.Prelude.Ord

type (<) a b = (:<) a b infix 4

type (<@#@$) = (:<$)

type (<@#@$$) = (:<$$)

type (<@#@$$$) a b = (:<$$$) a b

(%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b) infix 4

type (>) a b = (:>) a b infix 4

type (>@#@$) = (:>$)

type (>@#@$$) = (:>$$)

type (>@#@$$$) a b = (:>$$$) a b

(%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b) infix 4

type (<=) a b = (:<=) a b infix 4

type (<=@#@$) = (:<=$)

type (<=@#@$$) = (:<=$$)

type (<=@#@$$$) a b = (:<=$$$) a b

(%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b) infix 4

type (>=) a b = (:>=) a b infix 4

type (>=@#@$) = (:>=$)

type (>=@#@$$) = (:>=$$)

type (>=@#@$$$) a b = (:>=$$$) a b

(%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b) infix 4

type (/=) a b = (:/=) a b infix 4

type (/=@#@$) = (:/=$)

type (/=@#@$$) = (:/=$$)

type (/=@#@$$$) a b = (:/=$$$) a b

(%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b) infix 4

type (==) a b = (:==) a b infix 4

type (==@#@$) = (:==$)

type (==@#@$$) = (:==$$)

type (==@#@$$$) a b = (:==$$$) a b

(%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b) infix 4

type (+) a b = (:+) a b infixl 6

type (+@#@$) = (:+$)

type (+@#@$$) = (:+$$)

type (+@#@$$$) a b = (:+$$$) a b

(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6

type (-) a b = (:-) a b infixl 6

type (-@#@$) = (:-$)

type (-@#@$$) = (:-$$)

type (-@#@$$$) a b = (:-$$$) a b

(%-) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((-) a b) infixl 6

type * a b = (:*) a b infixl 7

type (*@#@$) = (:*$)

type (*@#@$$) = (:*$$)

type (*@#@$$$) a b = (:*$$$) a b

(%*) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing (* a b) infixl 7