Email Gateway (Aug 19 2022 at 10:13): Email Gateway (Aug 19 2022 at 10:13):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
Does the Quotient package works with record types? I'm beginning to suspect that it doesn't, because when I type ...
----8<---------------------
record my_record =
foo :: "nat"
bar :: "int"
declare [[mapQ3 my_record = (something,something_else)]]
----8<---------------------
... I get "Bad type name: my_record".
Thanks,
John
Email Gateway (Aug 19 2022 at 10:17):From: Brian Huffman <huffman@in.tum.de>
The problem here is that "my_record" is really just a type
abbreviation for "unit my_record_ext".
(Question for the other Isabelle developers: How is an ordinary user
supposed to discover what abbreviations like this stand for?)
I expect that the declaration should work with the "my_record_ext" type.
Email Gateway (Aug 19 2022 at 10:17):From: Peter Lammich <lammich@in.tum.de>
Good question! The best way that I know is inspecting the output of
ML_val {* @{typ my_record} |> dest_Type *}
Is there any simpler way?
Peter
Email Gateway (Aug 19 2022 at 10:17):From: Makarius <makarius@sketis.net>
It used to be just a type abbreviation many years ago, when I made the
first version of the record package with Wolfgang Naraschewski. Later the
package has acquired more and more features and sophistication, both for
syntax and proof tools.
Note that as plain type abbreviation, you would see the expansion
directly, which is sometimes not exactly desired, but would help here for
clarity. Since the record package puts its own syntax translation candy
over the basic type syntax it is hard to see to the bottom of it.
Anyway, using Isabelle/jEdit "CONTROL hover click" over the 'record'
keyword, or other means to get to ~~/src/HOL/Tools/record.ML, easily
reveals some (undocumented) configuration options. For example:
record my_record =
foo :: "nat"
bar :: "int"
declare [[record_type_abbr = false]]
declare [[record_type_as_fields = false]]
typ my_record
An old version of these options were mentioned in Isabelle2004/NEWS, but
they did not make it into the IsarRef manual so far.
I have also a question about quotients. The "Q3" seen above has passed by
several in times recently, but I did not find an explanation of it. Are
there now three quotient packages? Is there a chance to get back to just
one?
Makarius
Last updated: Apr 19 2024 at 08:19 UTC