Re: [isabelle] undefined & None
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] undefined & None
- From: Tjark Weber <webertj at in.tum.de>
- Date: Tue, 01 Oct 2013 11:03:54 +0200
- In-reply-to: <5249A17C.email@example.com>
- References: <17586634.60.1380549789223.JavaMail.Henri@Hammerklavier.local> <52498D1C.firstname.lastname@example.org> <987B82FE-C1A6-4549-84BB-66F1C655163B@gmail.com> <4C59F544-D15D-4A76-B4B6-AF8B62F4ECFB@cam.ac.uk> <2AF62C01-C7BB-4877-9615-7AA23B614854@gmail.com> <5249A17C.email@example.com>
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