Re: [isabelle] Separating function declaration from implementation
George Karabotsos writes:
> Hello all,
> I am wondering if there is a way to separate the declaration of a
> function (as defined by the fun or function keywords) by its implementation.
> This is possible using the older consts and primrec or refdef way for
> declaring functions but I cannot see how it can be done with the new way.
I noticed this too, and to take it one step further, why can't the
syntactic outlines of these tools be similar; i.e. just replace
"primrec" with "function". The reason I request this is that when
primrec fails (e.g. even on some primitive recursive functions in the
nominal package) I just switch to function. Why should this require
changing more than one keyword?
This archive was generated by a fusion of
Pipermail (Mailman edition) and