*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Nitpick: Output Syntax for Data Types*From*: Tjark Weber <tjark.weber at it.uu.se>*Date*: Fri, 9 May 2014 12:28:57 +0200

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

**Follow-Ups**:**Re: [isabelle] Nitpick: Output Syntax for Data Types***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Generated document doesn't compile with recent TeX Live.
- Next by Date: Re: [isabelle] Nitpick: Output Syntax for Data Types
- Previous by Thread: Re: [isabelle] Generated document doesn't compile with recent TeX Live.
- Next by Thread: Re: [isabelle] Nitpick: Output Syntax for Data Types
- Cl-isabelle-users May 2014 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list