Documentation

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

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

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

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

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

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

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