{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MagicHash #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnboxedTuples #-}

module Arithmetic.Equal
  ( symmetric
  , plusR
  , plusL
  , plusR#
  , plusL#
  , lift
  ) where

import Arithmetic.Unsafe (type (:=:) (Eq), type (:=:#) (Eq#))
import GHC.TypeNats (type (+))

symmetric :: (m :=: n) -> (n :=: m)
{-# INLINE symmetric #-}
symmetric :: forall (m :: Nat) (n :: Nat). (m :=: n) -> n :=: m
symmetric m :=: n
Eq = n :=: m
forall (a :: Nat) (b :: Nat). a :=: b
Eq

plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)
{-# INLINE plusL #-}
plusL :: forall (c :: Nat) (m :: Nat) (n :: Nat).
(m :=: n) -> (c + m) :=: (c + n)
plusL m :=: n
Eq = (c + m) :=: (c + n)
forall (a :: Nat) (b :: Nat). a :=: b
Eq

plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)
{-# INLINE plusR #-}
plusR :: forall (c :: Nat) (m :: Nat) (n :: Nat).
(m :=: n) -> (m + c) :=: (n + c)
plusR m :=: n
Eq = (m + c) :=: (n + c)
forall (a :: Nat) (b :: Nat). a :=: b
Eq

plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n)
{-# INLINE plusL# #-}
plusL# :: forall (c :: Nat) (m :: Nat) (n :: Nat).
(m :=:# n) -> (c + m) :=:# (c + n)
plusL# m :=:# n
_ = (# #) -> (c + m) :=:# (c + n)
forall (a :: Nat) (b :: Nat). (# #) -> a :=:# b
Eq# (# #)

plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c)
{-# INLINE plusR# #-}
plusR# :: forall (c :: Nat) (m :: Nat) (n :: Nat).
(m :=:# n) -> (m + c) :=:# (n + c)
plusR# m :=:# n
_ = (# #) -> (m + c) :=:# (n + c)
forall (a :: Nat) (b :: Nat). (# #) -> a :=:# b
Eq# (# #)

lift :: (m :=:# n) -> (m :=: n)
{-# INLINE lift #-}
lift :: forall (m :: Nat) (n :: Nat). (m :=:# n) -> m :=: n
lift m :=:# n
_ = m :=: n
forall (a :: Nat) (b :: Nat). a :=: b
Eq