Gergely Buday (Aug 08 2023 at 13:38): Gergely Buday (Aug 08 2023 at 13:38):Page 3 of the Datatype Tutorial shows the following example:
datatype 'a treefs = Node (lbl: 'a) (sub: " 'a treefs fset ")
where I omitted to subscripts. Someone told me that lbl and sub are ways out of this datatype: they are meant for getting the contents of a Node ... element. So I dared to write
datatype 'a dummy2 = "DummyConstructor (DummyOut:'a)"
but I got the error message
Legacy feature! Bad name binding: "dummy2.DummyConstructor (DummyOut:'a)"⌂
Bad name: "dummy2.DummyConstructor (DummyOut:'a)"
Is this really not possible anymore? Is there another way to get a constituent of a datatype without writing a function for it?
Wolfgang Jeltsch (Aug 08 2023 at 13:52):The problem is that you put the quotation marks around the whole datatype alternative specification. Quotation marks should only be put around types and terms. In your case, this would be just the type variable 'a, but for single names you don’t even need quotation marks.
Wolfgang Jeltsch (Aug 08 2023 at 14:00):By the way, the error message you quoted indicates that the error is not about defining selectors: it says that the whole block "dummy2.DummyConstructor (DummyOut:'a)" is a bad name, which makes it sort of clear that your code says that this block should be considered a single name.
Wolfgang Jeltsch (Aug 08 2023 at 14:02):I just remembered that there is another situation in which you have to use quotation marks: when writing theory names that contain characters usually not allowed in names, like HOL-Eisbach.Eisbach (the hyphen is the offender here and you surround the whole qualified name with quotation marks). Maybe Isabelle’s interpretation of your code above has to do with this use, as Isabelle considered the whole block delimited by quotation marks to be a single name.
Mathias Fleury (Aug 10 2023 at 15:43):(this behavior is consistent with shows Falsevs shows "P x", but you need to know what the parser is expecting, so it is consistent but not really intuitive)
Last updated: Apr 28 2024 at 12:28 UTC