*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] tail recursive definition*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Tue, 22 Feb 2011 20:48:50 +0100*Cc*: Jesus Aransay <jesus-maria.aransay at unirioja.es>, cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <166886C5-1873-41FA-A1FB-D824276095ED@gmail.com>*References*: <AANLkTinocA27W0HW852qLHxk0nWG0pSMmikH0nnKN2xA@mail.gmail.com> <166886C5-1873-41FA-A1FB-D824276095ED@gmail.com>*User-agent*: Mozilla-Thunderbird 2.0.0.22 (X11/20091109)

Hi Jesus,

function (tailrec) remove :: "'a set => (nat => 'a) => 'a set"where "remove A f = (if A = {} then A else remove (A - {f 1}) (%k.if k < (1::nat) then f k else f (Suc k)))"

When such a thing happens with a definitional package (e.g., "datatype", "inductive", "function"), it usually indicates a bug in the package. The "tailrec" option is seldom used or tested; a bug there wouldn't be so surprising.

Hope this helps. Alex

**References**:**[isabelle] tail recursive definition***From:*Jesus Aransay

**Re: [isabelle] tail recursive definition***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] tail recursive definition
- Next by Date: [isabelle] Call for Papers: Workshop on Automated Theory Engineering
- Previous by Thread: Re: [isabelle] tail recursive definition
- Next by Thread: [isabelle] Call for Papers: Workshop on Automated Theory Engineering
- Cl-isabelle-users February 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list