Changes between Version 80 and Version 81 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 6, 2008 4:27:55 AM (7 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) ==