Data.Type.Natural.Lemma.Arithmetic

Documentation

type Zero = 0

type One = 1

type S n = Succ n

sZero :: SNat 0

sOne :: SNat 1

data ZeroOrSucc n where

Constructors

IsZero :: ZeroOrSucc 0

IsSucc :: SNat n -> ZeroOrSucc (n + 1)

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

plusCongR :: SNat k -> (n :~: m) -> (k + n) :~: (k + m)

plusCongL :: (n :~: m) -> SNat k -> (n + k) :~: (m + k)

predCong :: (n :~: m) -> Pred n :~: Pred m

type Succ n = n + 1

sS :: SNat n -> SNat (Succ n)

sSucc :: SNat n -> SNat (Succ n)

type Pred n = n - 1

sPred :: SNat n -> SNat (Pred n)

sPred' :: proxy n -> SNat (Succ n) -> SNat n

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

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

multCongL :: (n :~: m) -> SNat k -> (n * k) :~: (m * k)

multCongR :: SNat k -> (n :~: m) -> (k * n) :~: (k * m)

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

minusCongL :: (n :~: m) -> SNat k -> (n - k) :~: (m - k)

minusCongR :: SNat k -> (n :~: m) -> (k - n) :~: (k - m)

succOneCong :: Succ 0 :~: 1

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

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

succNonCyclic :: SNat n -> (Succ n :~: 0) -> Void

induction :: forall p k. p 0 -> (forall n. SNat n -> p n -> p (S n)) -> SNat k -> p k

plusMinus :: SNat n -> SNat m -> ((n + m) - m) :~: n

plusMinus' :: SNat n -> SNat m -> ((n + m) - n) :~: m

plusZeroL :: SNat n -> (0 + n) :~: n

plusSuccL :: SNat n -> SNat m -> (S n + m) :~: S (n + m)

plusZeroR :: SNat n -> (n + 0) :~: n

plusSuccR :: SNat n -> SNat m -> (n + S m) :~: S (n + m)

plusComm :: SNat n -> SNat m -> (n + m) :~: (m + n)

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

multZeroL :: SNat n -> (0 * n) :~: 0

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

multSuccL' :: SNat n -> SNat m -> (S n * m) :~: ((n * m) + (1 * m))

multZeroR :: SNat n -> (n * 0) :~: 0

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

multComm :: SNat n -> SNat m -> (n * m) :~: (m * n)

multOneR :: SNat n -> (n * 1) :~: n

multOneL :: SNat n -> (1 * n) :~: n

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

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

minusNilpotent :: SNat n -> (n - n) :~: 0

multAssoc :: SNat n -> SNat m -> SNat l -> ((n * m) * l) :~: (n * (m * l))

plusEqCancelL :: SNat n -> SNat m -> SNat l -> ((n + m) :~: (n + l)) -> m :~: l

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

succAndPlusOneL :: SNat n -> Succ n :~: (1 + n)

succAndPlusOneR :: SNat n -> Succ n :~: (n + 1)

predSucc :: SNat n -> Pred (Succ n) :~: n

viewNat :: forall n. SNat n -> ZeroOrSucc n

zeroOrSucc :: SNat n -> ZeroOrSucc n

plusEqZeroL :: SNat n -> SNat m -> ((n + m) :~: 0) -> n :~: 0

plusEqZeroR :: SNat n -> SNat m -> ((n + m) :~: 0) -> m :~: 0

predUnique :: SNat n -> SNat m -> (Succ n :~: m) -> n :~: Pred m

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

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

minusZero :: SNat n -> (n - 0) :~: n

multEqCancelR :: forall n m l. SNat n -> SNat m -> SNat l -> ((n * Succ l) :~: (m * Succ l)) -> n :~: m

succPred :: SNat n -> ((n :~: 0) -> Void) -> Succ (Pred n) :~: n

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

pattern Zero :: () => n ~ 0 => SNat n

pattern Succ :: forall n n1. () => n ~ Succ n1 => SNat n1 -> SNat n