{-# language DataKinds #-}
{-# language ExplicitForAll #-}
{-# language KindSignatures #-}
{-# language TypeOperators #-}

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

import Arithmetic.Unsafe (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 = 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 = 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 = forall (a :: Nat) (b :: Nat). a :=: b
Eq