Re: [isabelle] "Unfolding" the sum-of-products encoding of datatypes
On Wed, 18 Nov 2015, Jasmin Blanchette wrote:
Overall, we managed to achieve very high levels of backward
compatibility and actually pulled it off. The ongoing "Nominal2" vs.
"Nominal" is reminder of how hard it is to subsume and replace an
existing Isabelle package. We (I) have made bona fide errors along the
way, but I think our record is remarkable and deserves more praise than
Definitely. I am impressed how the BNF datatype upgrade went through,
while the task was looking bigger and bigger as the years passed by. One
of the greatest engineering projects since Stonehenge!
This archive was generated by a fusion of
Pipermail (Mailman edition) and