GHC.TypeNats.Experimental
plusSNat :: SNat n -> SNat m -> SNat (n + m) Source #
timesSNat :: SNat n -> SNat m -> SNat (n * m) Source #
powerSNat :: SNat n -> SNat m -> SNat (n ^ m) Source #
minusSNat :: m <= n => SNat n -> SNat m -> SNat (n - m) Source #
divSNat :: 1 <= m => SNat n -> SNat m -> SNat (Div n m) Source #
modSNat :: 1 <= m => SNat n -> SNat m -> SNat (Mod n m) Source #
log2SNat :: 1 <= n => SNat n -> SNat (Log2 n) Source #