Changes between Version 69 and Version 70 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
08/27/08 16:10:36 (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeFunctionsSolving

    v69 v70  
    159159co1 :: F t1..tn ~ t  &  co2' :: t ~ s with co2 = co1 |> co2' 
    160160}}} 
    161  where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
     161 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.  '''SLPJ: why this restriction?  I thought we were treating 
     162flexible and rigid variables the same.''' 
    162163 
    163164 NB: Afterwards, we need to normalise `co2'`.  Then, the !SubstVarVar or !SubstVarFam rules may apply to the results of normalisation.  Moreover, `co1` may have a !SubstFam or a !SubstVarFam match with rules other than the results of normalising `co2'`.