{-# 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