Changes between Version 66 and Version 67 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 27, 2008 9:28:26 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v66 v67  
    151151 where `g :: forall x1..xm. F u1..um ~ s` and `[s1/x1, .., sm/xm]u1 == t1`. 
    152152 
     153 NB: Afterwards, we need to normalise.  Then, any of the four propagation rules may apply. 
     154 
    153155 '''!SubstFam''':: 
    154156{{{ 
     
    159161 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
    160162 
     163 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'`. 
     164 
    161165 '''!SubstVarVar''':: 
    162166{{{ 
     
    167171 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable. 
    168172 
    169  '''!SubstVarFam''':: 
     173 NB: Afterwards, we need to normalise `co2'`.  Then, the !SubstVarVar or !SubstVarFam rules may apply to the results of normalisation, but not with `co1`, as `s` and `t` cannot contain `x` - cf. the definition of normal equalities.  However, `co1` may have another !SubstVarVar or !SubstVarFam match with rules other than the results of normalising `co2'`. 
     174 
     175'''!SubstVarFam''':: 
    170176{{{ 
    171177co1 :: x ~ t  &  co2 :: F s1..sn ~ s