Re: [isabelle] Match exception in pat_completeness



Dear René,

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.

 -- Lars





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.