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

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