module Singleraeh.Natural where

import GHC.TypeNats
import Unsafe.Coerce ( unsafeCoerce )

infixl 6 %+
(%+) :: SNat n -> SNat m -> SNat (n + m)
SNat n
n %+ :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
%+ SNat m
m = Nat -> (forall (n :: Nat). SNat n -> SNat (n + m)) -> SNat (n + m)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
+ SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
m) SNat n -> SNat (n + m)
forall (n :: Nat). SNat n -> SNat (n + m)
forall a b. a -> b
unsafeCoerce

infixl 6 %-
(%-) :: SNat n -> SNat m -> SNat (n - m)
SNat n
n %- :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
%- SNat m
m = Nat -> (forall (n :: Nat). SNat n -> SNat (n - m)) -> SNat (n - m)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
- SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
m) SNat n -> SNat (n - m)
forall (n :: Nat). SNat n -> SNat (n - m)
forall a b. a -> b
unsafeCoerce

infixl 7 %*
(%*) :: SNat n -> SNat m -> SNat (n * m)
SNat n
n %* :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
%* SNat m
m = Nat -> (forall (n :: Nat). SNat n -> SNat (n * m)) -> SNat (n * m)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n Nat -> Nat -> Nat
forall a. Num a => a -> a -> a
* SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
m) SNat n -> SNat (n * m)
forall (n :: Nat). SNat n -> SNat (n * m)
forall a b. a -> b
unsafeCoerce

sMod :: SNat n -> SNat m -> SNat (Mod n m)
sMod :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Mod n m)
sMod SNat n
n SNat m
m = Nat
-> (forall (n :: Nat). SNat n -> SNat (Mod n m)) -> SNat (Mod n m)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
mod (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n) (SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
m)) SNat n -> SNat (Mod n m)
forall (n :: Nat). SNat n -> SNat (Mod n m)
forall a b. a -> b
unsafeCoerce

sDiv :: SNat n -> SNat m -> SNat (Div n m)
sDiv :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Div n m)
sDiv SNat n
n SNat m
m = Nat
-> (forall (n :: Nat). SNat n -> SNat (Div n m)) -> SNat (Div n m)
forall r. Nat -> (forall (n :: Nat). SNat n -> r) -> r
withSomeSNat (Nat -> Nat -> Nat
forall a. Integral a => a -> a -> a
div (SNat n -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat n
n) (SNat m -> Nat
forall (n :: Nat). SNat n -> Nat
fromSNat SNat m
m)) SNat n -> SNat (Div n m)
forall (n :: Nat). SNat n -> SNat (Div n m)
forall a b. a -> b
unsafeCoerce