| 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