5 Aug
2011
5 Aug
'11
11:57 a.m.
2011/8/5 Brent Yorgey
Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like.
I realiser the offer wasn't for me but yes, please, I'd like to know how you could do that, also with a subtract function example, and with a user input example. Pretty please ? David