Skip to content

Instantly share code, notes, and snippets.

@deque-blog

deque-blog/MoneyAdd2.idr

Last active August 16, 2017 12:42
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save deque-blog/29adf17c453c5fb8a9893b406d8c4e5a to your computer and use it in GitHub Desktop.
Save deque-blog/29adf17c453c5fb8a9893b406d8c4e5a to your computer and use it in GitHub Desktop.
Download ZIP
Raw
MoneyAdd2.idr
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