[isabelle-dev] copy_bnf

[Lars Hupel]

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/>