| 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 |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment