Re: [isabelle] undefined & None

On Mon, 2013-09-30 at 18:06 +0200, Andreas Lochbihler wrote:
> I agree that undefined is unfortunate, and unspecified would probably
> be a better name.


> "undefined" is frequently used by packages (primrec, function,
> partial_function) in cases where the user has not given a full
> specification of a constant.

I am not sure how widespread this usage still is in Isabelle. But where
it happens, I consider it a (minor) shortcoming, because it leads to
spurious equations: the user arguably never intended to specify that,
e.g., "hd [] = last []".


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