Changes between Version 22 and Version 23 of NewAxioms/Nonlinearity


Ignore:
Timestamp:
May 30, 2013 3:37:11 PM (11 months ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • NewAxioms/Nonlinearity

    v22 v23  
    4343}}} 
    4444These would be considered overlapping by (A), but accepted as non-overlapping (ie unification fails) by (B).  And indeed these two are fine (ie cannot give rise to unsoundness). 
     45 
     46Intuition: under (B) the only way that unification fails is because of a definite conflict (eg `Int` ~ `Bool`).  And unification failing is what allows us to accept the two equations as non-overlapping.  So if we accept them, they have a definite conflict. 
    4547 
    4648== Problem: coincident overlap ==