Changes between Version 4 and Version 5 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 22, 2008 7:48:58 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v4 v5  
    2121== Normalisation == 
    2222 
     23 * Perform Rule Triv as part of normalisation. 
    2324 * Whenever an equality of Form (2) or (3) would be recursive, the program can be rejected on the basis of a failed occurs check.  (Immediate rejection is always justified, as right-hand sides do not contain synonym familles; hence, any recursive occurrences of a left-hand side imply that the equality is unsatisfiable.) 
    2425