by James Chapman on November 18, 2005.
Tagged as: Lunches.
The other day I tried to write division on natural numbers in epigram. This function is not obviously structurally recursive so we cannot use the standard justification ‘<=rec ‘ to justify our recursive calls and also leave our function looking like the one we wanted to write in the first place. We can exhibit a view to do a custom case analysis that does the necessary subtraction for us yielding patterns of arguments to ‘plus’ (this is the Compare view from VFL). We can then exhibit another view to justify the recursive call on an argument to ‘plus’. I found a likely candidate in Edwin Brady’s thesis and Conor informed me that it first saw the light of day in a talk by James McKinna in 2002. It’s called ‘PlusRec’ and I don’t understand it.