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.

+1

> "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 []".

Best,
Tjark






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