Moduleghc-experimental-10.0.0Haskell2010

GHC.TypeNats.Experimental

valueplusSNat :: SNat n -> SNat m -> SNat (n + m)

valuetimesSNat :: SNat n -> SNat m -> SNat (n * m)

valuepowerSNat :: SNat n -> SNat m -> SNat (n ^ m)

valueminusSNat :: m <= n => SNat n -> SNat m -> SNat (n - m)

valuedivSNat :: 1 <= m => SNat n -> SNat m -> SNat (Div n m)

valuemodSNat :: 1 <= m => SNat n -> SNat m -> SNat (Mod n m)

valuelog2SNat :: 1 <= n => SNat n -> SNat (Log2 n)