Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer



On Mon, Oct 19, 2015 at 7:18 PM, Thomas Genet <thomas.genet at irisa.fr> wrote:

>
>
> Le 19/10/2015 14:55, Rustom Mody a Ãcrit :
>
>> Thanks for that Thomas!
>> Just one point -- I had to change the fun to primrec... Not sure I
>> understand why but saw that somewhere and tried
>>
>
> Dear Rustom,
>
>
> you can define remove using "primrec" since it is a primitive recursive
> function.
>
> However, you should be able to define it using "fun" since "fun" accepts a
> superset of functions, including primitive recursive ones.
>
>
>
fun give this error

constants
  remove :: "'a â 'a list â 'a list"
Found termination order: "(Îp. length (snd p)) <*mlex*> {}"



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