[developers] LKB vs. PET divergences

John Carroll J.A.Carroll at sussex.ac.uk
Mon Feb 14 15:57:14 CET 2005

> Alternatively, we have a discrepancy in the glb calculation algorithm, 
> which
> would also be possible, though horrible to fix.  If there's a formal
> definition of glbtype introduction which says whether it is or is not 
> supposed
> to introduce pure types in this situation, then we can decide which 
> behaviour
> is correct.

I also don't have PET available to check, but if the two systems start 
with the same type hierarchy and then introduce glbs I'd be surprised 
if they came out with substantively different results. There's just not 
much freedom to do things differently, or incorrectly.


More information about the developers mailing list