Re: [isabelle] Match exception in pat_completeness
the following code
function foo :: "'a list ⇒ nat" where
"foo (y # ys) = 0"
by pat_completeness termination sorry
raises a Match exception in pat_completeness (in Isabelle 2009-2):
*** exception Match raised (line 111 of
pat_completeness is behaving badly here, and throws a low-level
exception. The correct behaviour would be
"empty result sequence"
since your patterns are indeed incomplete, and it wont be able to prove
completeness. (Look at the first subgoal that it is supposed to solve).
The function package can add the missing pattern automatically, if you
pass it the "(sequential)" option (which is also implicit when you use
the abbreviated form "fun". If your real problem is as simple as this
one, then you probably want to use "fun".
More explanations can be found in the tutorial for function definitions:
*** At command "by".
This archive was generated by a fusion of
Pipermail (Mailman edition) and