Re: [isabelle] Data‑types: How to use discriminators?



On Mon, 09 Dec 2013 10:46:01 +0100, Jasmin Blanchette <jasmin.blanchette at gmail.com> wrote:

Hi Yannick,

Also I noticed “datatypes.pdf” talks about “datatype_new” and some others, which seems not to be recognized. Is this an error or something old or something new to come?

The answer is in the introduction of that document (p. 4):

To use the package, it is necessary to import the BNF theory, which can be precompiled into the HOL-BNF image. The following commands show how to launch jEdit/PIDE with the image loaded and how to build the image without launching jEdit:

    isabelle jedit -l HOL-BNF
    isabelle build -b HOL-BNF

I missed it (as it was not my first time in “datatypes.pdf”, I missed this change in the introduction). Also HOL-BNF can be selected as the default image in jEdit.

Now there are theorems “t.discI(n)” which indeed do what's needed. The functions “t.is_Cn” do the same as explicitly defined functions (in a prior message).

Is it OK to use HOL-BNF or is it still subject to big change? What would you recommend between “datatype” and “datatype_new”?

--
Yannick Duchêne




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