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



Am 07.11.2013 16:29, schrieb Gottfried Barrow:
However, if one of the BNF crew cares, below is what I get, which could be due to me doing things wrong, or not knowing how to register something to make it work. I give an example of "value" returning an error, where I know that "value" and the code generator can be a whole different matter.
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).

Dmitriy



datatype_new 'a mS =
mSp "'a * int"
|mSS "'a mS fset"

primrec_new mSSsome :: "'a mS => 'a mS fset option" where
"mSSsome (mSp x) = None"
|"mSSsome (mSS x) = Some x"

theorem "mSSsome (mSS{|mSp x|}) = Some {|mSp x|}"
by(simp)

theorem "mSSsome (mSp x) = None"
by(simp)

value "mSSsome (mSp x)"
(*ERROR:
"c.mS.mSp" is not a constructor, on left hand side of equation, in theorem:
mSSsome (mSp ?x) ≡ None*)





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