[isabelle] Nitpick: Output Syntax for Data Types



Jasmin (et al.),

Consider the following minimal example:

theory Scratch imports Main
begin
  datatype t = A | B
  lemma "(x::t) = y"
    nitpick
  oops
end

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".

Best,
Tjark






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