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 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) => 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)

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

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