Changes between Version 55 and Version 56 of TypeFunctionsSolving


Ignore:
Timestamp:
Aug 17, 2008 9:10:30 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v55 v56  
    4141 2. '''Variable equality:''' `co :: x ~ t`, where we again distinguish two forms: 
    4242  a. '''Variable-term equality:''' `co :: x ~ t`, where `t` is ''not'' a variable, or 
    43   b. '''Variable-variable equality:''' `co :: x ~ y`, where `x < y`. 
     43  b. '''Variable-variable equality:''' `co :: x ~ y`, where `x > y`. 
    4444 
    4545where 
     
    4747 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 
    4848 * the left-hand side of an equality may not occur in the right-hand side, and 
    49  * the relation `x < y` is a total order on type variables, where `alpha < a` whenever `alpha` is a flexible and `a` a rigid type variable (otherwise, the total order may be aribitrary). 
     49 * the relation `x > y` is a total order on type variables, where `alpha > a` whenever `alpha` is a flexible and `a` a rigid type variable (otherwise, the total order may be aribitrary). 
    5050 
    5151The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left- and right-hand sides are different. 
     
    116116    .. 
    117117    (tn', eqtn) = flatten tn 
    118     FRESH alpha 
     118    FRESH alpha, such that alpha > x for all x already used 
    119119    RECORD alpha := F t1'..tn' 
    120120flatten [[t1 t2]] = (t1' t2', eqs++eqt)