Re: [isabelle] Match exception in pat_completeness
On 23.07.2010 10:25, René Thiemann wrote:
since you do not give all patterns (there is no case for the empty list),
you have to pass the sequential argument to the definition.
yes, this function definition is not complete, which is obvious here.
But it was far from obvious in my original function definition (from
which I extracted this toy example). Hence I would expect
pat_completeness to fail gracefully (or generate unsatisfiable
constraints), so the user can see that it is not a bug in Isabelle, but
his definition is wrong.
This archive was generated by a fusion of
Pipermail (Mailman edition) and