Changes between Version 66 and Version 67 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 27, 2008 9:28:26 AM (7 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