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 higher-order datatypes (think Ordinals), which fun's automated
termination provers cannot handle, since they only use measures into nat.
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
