Changes between Version 51 and Version 52 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 16, 2008 5:13:00 AM (7 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v51 v52  
    121121 * Perform Rule Triv as part of normalisation.
    122122 * 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.)
    123  * 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.)
    124 
    125 
    126 == Solving ==
     123 * 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`.)
     124
     125
     126== Propagation (aka Solving) ==
    127127
    128128A significant difference to new-single is that solving is a purely local operation.  We never instantiate any flexible variables.