Documentation

plusSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m) Source #

timesSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m) Source #

powerSNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m) Source #

minusSNat :: forall (m :: Nat) (n :: Nat). m <= n => SNat n -> SNat m -> SNat (n - m) Source #

divSNat :: forall (m :: Natural) (n :: Nat). 1 <= m => SNat n -> SNat m -> SNat (Div n m) Source #

modSNat :: forall (m :: Natural) (n :: Nat). 1 <= m => SNat n -> SNat m -> SNat (Mod n m) Source #

log2SNat :: forall (n :: Natural). 1 <= n => SNat n -> SNat (Log2 n) Source #