Re: [isabelle] Non-exhaustive case certificates

Hi Andreas,

>> Case certificates must always be exhaustive!
> Exhaustive with respect to what?

exhaustive in the sense that the number of discriminators must be
*equal* to the number of constructors (in the sense of the code generator).

> I do not see why
> code certificates need to be exhaustive with respect to the logic other
> than restrictions in the code generator implementation.

True.  The implementation however is not so general since in my mind I
could never imagine a user case which would make it necessary to provide
anything beyond the internal foundational case certificates as a kind of
protocol between the datatype package and the code generator.  This is
the reason why there is no full-blown user interface for case
certificates (yet).  Indeed two years ago I was thinking about that but
put it aside since it did not seem worth the effort.

The best documentation for case certificates available is indeed if you
follow the implementation of Code.add_case.

What is your application?  Does it go beyond pure esthetic concerns?  I
would be relucant to touch the trusted code base of code.ML if there is
not a striking reason (neglecting questions of effort estimation at the



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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