Dear Dmitriy,
I like the new "copy_bnf" command a lot, especially to allow records to
be used in nested recursion. However, after a record definition, I have
to invoke the command manually*. I would like to propose that "record"
gains an option to call it directly. So, instead of writing:
record 'a foo = bla :: 'a
copy_bnf ('a, 'b) foo_ext
... I could write
record (copy_bnf) 'a foo = bla :: 'a
Depending on the efficiency of the internal constructions "copy_bnf"
could also be the default.
I do have a use case for this: Lem** is able to generate Isar sources
containing records, and in CakeML, these records are then used for
nested recursion. Lem could be changed to emit an additional "copy_bnf",
but that would make it dependent on the internal construction ("_ext").
Hence, I would much prefer a flag or to run it by default.
Cheers
Lars
* and to remember that I need to use "foo_ext" because otherwise I get
an ML exception
** <https://bitbucket.org/Peter_Sewell/lem/>
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
