Skip to content

Instantly share code, notes, and snippets.

What would you like to do?
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