Re: [isabelle] function (tailrec,sequential) fails



Hi Joachim,

These problems with "tailrec" are starting to become embarrasing for me. :-}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
theory Tmp imports Main
begin

function (sequential,tailrec) f where "f True = 0"
  apply pat_completeness
  apply auto
done
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

gives me:

*** Tactic failed.
*** The error(s) above occurred for the goal statement:
*** f_sumC False = undefined
*** At command "done".

I just pushed a quick fix, which seems to help here, and also makes your real example go through:

http://isabelle.in.tum.de/repos/isabelle/rev/39db63c45683

The patch also works for the Isabelle2009-2 release.

Hope this helps...

Alex






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