Re: [isabelle] Match exception in pat_completeness



Dear Lars,

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.

function (sequential) foo :: "'a list ⇒ nat" where
     "foo (y # ys) = 0"
   by pat_completeness auto
termination ...

However, for such a simple function you can also directly use fun, since it
will figure out the termination proof by itself.

fun foo :: "'a list ⇒ nat" where
  "foo (y # ys) = 0"


Best regards,
René

Am 22.07.2010 um 14:57 schrieb Lars Noschinski:

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.