Re: [isabelle] Nitpick: Output Syntax for Data Types



Hi Tjark,

> Here, the output that I get from Nitpick is "x = t⇩1 y = t⇩2". I would
> have preferred to see, e.g., "x = A y = B". 
> 
> Incidentally, the latter is what (the now-ancient) Refute prints. And
> even Nitpick uses proper constructor names when the lemma is "x = A".

This is due to an optimization. If the constructors don't appear in the problem (including definitional axioms etc.), Nitpick treats the datatype as an uninterpreted type (but with the right cardinality constraints), thereby keeping the translation simple. It would be possible for Nitpick to generate some constructor terms instead of t1 and t2, but apart from the fact that it's simpler to generate t1 and t2, I find the added generality nicer, because it indicates that the actual choice of values is irrelevant.

Cheers,

Jasmin





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