Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/MoneyAdd.idr

Last active Aug 14, 2017
Embed
What would you like to do?
record Money where -- Definition of Money
constructor MkMoney -- * With a constructor named MkMoney
currency : Currency -- * Containing a currency
amount : Amount -- * And an amount of money
-- Definition of `add` which takes 2 Money instances and returns a new one
add : (m1, m2 : Money) -> Money
add m1 m2 = MkMoney (currency m1) (amount m1 + amount m2)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment