Changes between Version 51 and Version 52 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 16, 2008 5:13:00 AM (6 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.