[isabelle] Nitpick: Output Syntax for Data Types
Jasmin (et al.),
Consider the following minimal example:
theory Scratch imports Main
datatype t = A | B
lemma "(x::t) = y"
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 archive was generated by a fusion of
Pipermail (Mailman edition) and