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
exceedingly obvious.

> 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 MHonArc.