[isabelle] Match exception in pat_completeness



Hello,

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 "/var/tmp/isabelle-makebin14768/Isabelle2009-2/src/HOL/Tools/Function/pat_completeness.ML")
  *** At command "by".

-- Lars





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