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 :: nat) where Source #
IsZero :: ZeroOrSucc (Zero nat) | |
IsSucc :: Sing n -> ZeroOrSucc (Succ n) |
class (SDecide nat, SNum nat, SEnum nat, SingKind nat, SingKind 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 #
toNatural :: Sing (n :: nat) -> Natural Source #
fromNatural :: Natural -> SomeSing nat Source #
pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n Source #
module Data.Singletons.Prelude.Eq
module Data.Singletons.Prelude.Num
module Data.Singletons.Prelude.Ord
(%<) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<) a b) infix 4 Source #
(%>) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>) a b) infix 4 Source #
type (<=@#@$$$) a b = (:<=$$$) a b Source #
(%<=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((<=) a b) infix 4 Source #
type (>=@#@$$$) a b = (:>=$$$) a b Source #
(%>=) :: forall nat (a :: nat) (b :: nat). SOrd nat => Sing a -> Sing b -> Sing ((>=) a b) infix 4 Source #
type (/=@#@$$$) a b = (:/=$$$) a b Source #
(%/=) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((/=) a b) infix 4 Source #
type (==@#@$$$) a b = (:==$$$) a b Source #
(%==) :: forall nat (a :: nat) (b :: nat). SEq nat => Sing a -> Sing b -> Sing ((==) a b) infix 4 Source #
(%+) :: forall nat (a :: nat) (b :: nat). SNum nat => Sing a -> Sing b -> Sing ((+) a b) infixl 6 Source #