Changes between Version 67 and Version 68 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 27, 2008 9:44:29 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v67 v68  
    171171 where `co1` is local, or both `co1` and `co2` are wanted and at least one of the equalities contains a flexible variable.
    172172
    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'`.
     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'`.
    174174
    175175'''!SubstVarFam'''::
     
    179179co1 :: x ~ t  &  co2' :: [t/x](F s1..sn) ~ s with co2 = [co1/x](F s1..sn) |> co2'
    180180}}}
    181 where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.)
     181 where `x` occurs in `F s1..sn`.  (`co1` may be local or wanted.)
     182
     183 NB: No normalisation required.  Afterwards, !SubstVarVar or !SubstVarFam may apply to `co1` and all rules, except !SubstVarVar, may apply to `co2'`.  However, !SubstVarFam cannot again apply to `co1` and `co2'`, as `t` cannot contain `x` -- cf. the definition of normal equalities..
    182184
    183185=== Rule application: specification ===