Re: [isabelle] Declaring equal for a type; BNF not working on the left

On 11/7/2013 11:01 AM, Jasmin Blanchette wrote:
Once the next release is out, one of our first priorities will be to make sure "fun", the code generator, Quickcheck, Nitpick, etc., work with "datatype_new" just like they do with "datatype". We're currently waiting to avoid too much divergence between the release branch (from which the release candidates are generated) and the development branch (which will lead to the next-to-next Isabelle release).


Alright, sounds good. Sledgehammer is my friend.

On 11/7/2013 3:14 PM, Dmitriy Traytel wrote:
In this case it is simply the case that the new datatypes are not yet registered in the code generator. A simple

code_datatype mSp mSS

will make the "value" command work for now. There is some more useful default code generator setup (see e.g. $AFP/thys/Coinductive/Coinductive_List) that is as well on our agenda (to make it happen automatically) as the interaction with fun (as Jasmin mentioned).


Thanks. One error leads to another. That got me to the usual type of errors:

Wellsortedness error:
Type 'a∷type mS not of sort equal
No type arity mS :: equal

I might figure out how to fix that someday. On the other hand, my type mT, which is based on lists rather than fsets, doesn't give me that error, so it's just easier to go with the magic.

On 11/7/2013 3:32 PM, Gottfried Barrow wrote:
...I looked at [2] a little, but without knowing the advantages of either, I'd pick [2] over [1].

That should have been [1] over [2].

I put me an assumes axiom in a local like this:
assumes mTeq_ax: "mTeq == HOL.eq"

I guess it should be obvious that I wouldn't want the axiom "mTeq x y <-> x = y" anywhere, since I'll commonly have "mTeq x y = True" when I have "HOL.eq x y = False". I suppose that's the difference between starting with a new type where you make all the rules, and a type you use which already has lots of rules with it.


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