I want to add:
It is still used
(a) for didactical reasons, to teach primitive recursion over datatypes,
(a') to clearly indicate what the corresponding induction rule is.
Florian
--
Home:
http://www.in.tum.de/~haftmann
PGP available:
Hi Brian,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: nat = nat where
foo 0 = 1 | foo (Suc n) = foo 0
*** Extra variables on rhs: foo
*** The error(s) above occurred in definition
What is the status of primrec anyway, in the light of fun(ction)?
It is still used
(a) for didactical reasons, to teach primitive recursion over datatypes,
(b) for bootstrapping purposes within HOL-Plain,
(c) since it is faster than fun, as it merely instantiates a combinator, and
(d) for
Hello all,
I just noticed this error message from primrec if you write a
specification that is not primitive recursive. Here is a simplified
example:
primrec foo :: nat = nat where
foo 0 = 1 | foo (Suc n) = foo 0
*** Extra variables on rhs: foo
*** The error(s) above occurred in definition
On Sat, 2011-05-21 at 15:12 -0700, Brian Huffman wrote:
I just noticed this error message from primrec [...]
What is the status of primrec anyway, in the light of fun(ction)?
Kind regards,
Tjark
___
isabelle-dev mailing list
isabelle-...@in.tum.de
