Changes between Version 68 and Version 69 of TypeFunctionsSolving


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

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v68 v69  
    173173 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 
    175 '''!SubstVarFam''':: 
     175 '''!SubstVarFam''':: 
    176176{{{ 
    177177co1 :: x ~ t  &  co2 :: F s1..sn ~ s