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