Re: [isabelle] Proof of concept: BNF-based records
> Can you explain this further? Is there an inherent problem of the
> general idea of the regular record package wrt. BNFs? Can the BNF
> experts comment on that?
I explained that in my email. "copy_bnf" makes a record a BNF. But for
it to be able to be used in a function definition, it also requires size
setup, which as of now, is manual.
> BTW, there is an old Isabelle development principle to be monotonic wrt.
> existing tools. A fork and clone is bad enough, one that disrupts what
> is already there is worse: entropy, decay.
As I said, raw syntax cannot be bundled. I expect people to have a brief
look over what they're including, and the way the syntax setup works is
> This hints at various discussions in the dark. We have relatively little
> traffic on the isabelle-users and isabelle-dev mailing lists, so why not
> use them for proper discussions?
The problems with record + nested recursion had been laid out on the
mailing lists a few months ago.
This archive was generated by a fusion of
Pipermail (Mailman edition) and