sameCurrency.idr

data SameCurrency : (m1, m2: Money) -> Type where
  MkSameCurrency : (currency m1 = currency m2) -> SameCurrency m1 m2

sameCurrency : (lhs, rhs : Money) -> Dec (SameCurrency lhs rhs)
sameCurrency lhs rhs =
  case decEq (currency lhs) (currency rhs) of
    Yes prf => Yes (MkSameCurrency prf)
    No contra => No $ \(MkSameCurrency sameCurr) => contra sameCurr