Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/MoneyAdd2.idr

Last active Aug 16, 2017
Embed
What would you like to do?
add :
(m1, m2 : Money) -- Arguments of the function: 2 Money instances
-> {auto prf : SameCurrency m1 m2} -- Proof that m1 and m2 have the same currency
-> Money -- Return type: a new Money instance
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment