Changes between Version 55 and Version 56 of TypeFunctionsSolving
 Timestamp:
 Aug 17, 2008 9:10:30 AM (7 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v55 v56 41 41 2. '''Variable equality:''' `co :: x ~ t`, where we again distinguish two forms: 42 42 a. '''Variableterm equality:''' `co :: x ~ t`, where `t` is ''not'' a variable, or 43 b. '''Variablevariable equality:''' `co :: x ~ y`, where `x <y`.43 b. '''Variablevariable equality:''' `co :: x ~ y`, where `x > y`. 44 44 45 45 where … … 47 47 * the types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families, 48 48 * the lefthand side of an equality may not occur in the righthand 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). 50 50 51 51 The second bullet of the where clause is trivially true for equalities of Form (1); it also implies that the left and righthand sides are different. … … 116 116 .. 117 117 (tn', eqtn) = flatten tn 118 FRESH alpha 118 FRESH alpha, such that alpha > x for all x already used 119 119 RECORD alpha := F t1'..tn' 120 120 flatten [[t1 t2]] = (t1' t2', eqs++eqt)