Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/sameCurrency.idr

Last active August 19, 2017 18:02
Show Gist options
  • Star 1 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save deque-blog/3ab28028c16895eba4536a188d70b1e6 to your computer and use it in GitHub Desktop.
Save deque-blog/3ab28028c16895eba4536a188d70b1e6 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment