Safe Haskell | None |
---|---|
Language | Haskell2010 |
Documentation
type family Zero nat :: nat where ... Source #
Zero nat = FromInteger 0 |
type family One nat :: nat where ... Source #
One nat = FromInteger 1 |
data ZeroOrSucc n where Source #
IsZero :: ZeroOrSucc (Zero nat) | |
IsSucc :: Sing n -> ZeroOrSucc (Succ n) |
class (SDecide nat, SNum nat, SEnum nat) => IsPeano nat where Source #
succOneCong, succNonCyclic, predSucc, plusMinus, succInj, (plusZeroL, plusSuccL | plusZeroR, plusZeroL), (multZeroL, multSuccL | multZeroR, multSuccR), induction
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 #