[Agda] Dependent Types at Work

[Peter Dybjer]

Dear Tristan,

We really meant that the exercise would simply be to define "cut-off
subtraction" (or "monus" as my logic teacher called it), where you return
0 if the second argument is greater than or equal to the first. This is a
standard exercise when learning how to develop mathematics using primitive
recursive functions.

But our text only says "subtraction" which is of course a bit misleading.
Thanks for pointing this out!

There are many variations, like Dan's, where

>>   subtraction is only defined for second arguments less in
>>   value than or equal in value to the first argument

but at that early stage in the notes we don't expect the reader to be
quite ready for such considerations.  Such an exercise could be added a
little later after we have got into propositions as types.

Best wishes,
Peter