We need to figure out how recdef does it. The minimum number of equations is
mathematically fixed, so recdef must be using conditional expressions or other
tricks.
Larry
On 9 Jun 2015, at 23:07, Gerwin Klein gerwin.kl...@nicta.com.au wrote:
I can confirm that, at least that side is simple.
Function and recdef work very differently. Function first disambiguates
the patterns, then it defines the graph of the function as an inductive
definition. Recdef turns the definitions into a single recursion equation with
case-expressions on the rhs.
Concerning the minimum number of
