Changes between Version 48 and Version 49 of TypeFunctionsSolving
 Timestamp:
 Aug 16, 2008 4:16:06 AM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v48 v49 41 41 * 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). 42 42 43 The second bullet of the where clause is trivially true for equalities of Form (1) and itimplies that the left and righthand sides are different.43 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. 44 44 45 45 Furthermore, we call a variable equality whose lefthand side is a flexible type variable (aka unification variable) a '''flexible variable equality''', and correspondingly, a variable equality whose lefthand side is a rigid type variable (aka skolem variable) a '''rigid variable equality.'''