As somebody who’s wasted a week trying to do this, I can’t say that I like it myself.
Larry > On 20 Aug 2020, at 21:27, Bertram Felgenhauer > <[email protected]> wrote: > > Hi, > > I've gotten some emails from Jenkins lately and finally taken a moment > to investigate. > > Apparently, R1 <*lex*> R2 was changed to artificially impose > irreflexivity on R1 (checking a ~= a' in addition to a R1 a'). > > What are the benefits of doing this? There is a (heavy, to me) > downside: It destroys the property that the lexicographic product is > transitive if both input relations are. More fundamentally, while in > the previous formulation, the lexicographic product was a meaningful > and useful operation for quasi-orders, now that use case is closed > off. > > Was this change discussed in advance? I may have missed it... in any > case I strongly dislike it. > > Cheers, > > Bertram > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
