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