Changes between Version 31 and Version 32 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 4, 2008 12:11:59 PM (6 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v31 v32  
    4545 * We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables. 
    4646 * Normal equalities are similar to equalities meeting the Orientation Invariant and Flattening Invariant of new-single, but they are not the same. 
    47  * Normal equalities are '''never''' recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities. 
     47 * Normal equalities are '''never''' self-recursive.  They can be mutually recursive.  A mutually recursive group will exclusively contain variable equalities.  '''SLPJ''' why.  What prevents `a ~ [b], b ~ [a]`?   
    4848 
    4949=== Coercions === 
     
    5757Moreover, `TcTyFuns.RewriteInst` represents normal equalities, emphasising their role as rewrite rules.  
    5858 
     59'''SLPJ''': I propose that we use a proper data type, not `Either` for this. 
    5960 
    6061== Normalisation ==