*To*: Gottfried Barrow <gottfried.barrow at gmx.com>*Subject*: Re: [isabelle] Declaring equal for a type; BNF not working on the left*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Thu, 07 Nov 2013 22:14:41 +0100*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <527BB1D1.1050302@gmx.com>*References*: <527B1BB1.3090708@gmx.com> <527BB1D1.1050302@gmx.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.1.0

Am 07.11.2013 16:29, schrieb Gottfried Barrow:

However, if one of the BNF crew cares, below is what I get, whichcould be due to me doing things wrong, or not knowing how to registersomething to make it work. I give an example of "value" returning anerror, where I know that "value" and the code generator can be a wholedifferent matter.

code_datatype mSp mSS

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, intheorem:mSSsome (mSp ?x) ≡ None*)

**References**:**[isabelle] Declaring equal for a type; BNF not working on the left***From:*Gottfried Barrow

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

- Previous by Date: Re: [isabelle] (structure) and \<index>
- Next by Date: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Previous by Thread: Re: [isabelle] Declaring equal for a type; BNF not working on the left
- Next by Thread: [isabelle] Additional type variable(s) in specification
- Cl-isabelle-users November 2013 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