Changes between Version 80 and Version 81 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 4:27:55 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v80 v81  
    7474== Normalisation == 
    7575 
    76 The following function `norm` turns an arbitrary equality into a set of normal equalities.  As in `new-single`, the evidence equations are differently interpreted depending on whether we handle a wanted or local equality. 
     76The following function `norm` turns an arbitrary equality into a set of normal equalities. 
    7777{{{ 
    7878data EqInst         -- arbitrary equalities 
     
    134134 
    135135Notes: 
    136  * Perform Rule Triv as part of normalisation. 
     136 * Perform Rule Triv & Decomp as part of normalisation. 
    137137 * 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.) 
    138  * We flatten locals and wanteds in the same manner, using fresh flexible type variables.  (We have flexibles in locals anyway and don't use (Unify) during normalisation - this is different to `new-single`.) 
    139  
    140138 
    141139== Propagation (aka Solving) ==