[isabelle-dev] unhelpful low-level error message from primrec

Alexander Krauss krauss at in.tum.de
Sun May 22 19:40:58 CEST 2011


> 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



More information about the isabelle-dev mailing list