Re: [isabelle] undefined & None
> > "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 ".
However, this comes in handy in some cases. Consider, e.g., the
assumes A: "map f l = map f l'"
shows "f (l!i) = f (l'!i)"
without knowing that nth is undefined if the index is out of bounds,
this lemma would have a precondition (i<length l) which makes it harder
to be used by the simplifier.
This archive was generated by a fusion of
Pipermail (Mailman edition) and