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
Thanks. One error leads to another. That got me to the usual type of errors:
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  a little, but without knowing the advantages of
either, I'd pick  over .
That should have been  over .
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