Changes between Version 13 and Version 14 of TypeFunctionsSolving

Show
Ignore:
Timestamp:
07/30/08 08:14:47 (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • TypeFunctionsSolving

    v13 v14  
    1313 
    1414The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families.  Moreover, in Forms (2) & (3), the left- and right-hand side need to be different, and the left-hand side may not occur in the right-hand side. 
     15 
     16'''SLPJ''': Terminology: I think "flexible type variable" = "unification variable" = "HM variable". 
     17 
     18'''SLPJ''': I think that you intend a "normal equality" to embody the Orientation Invariant and the Flattening Invariant from new-single.tex.  But they don't line up exactly.  For example, what about `F [x] ~ G x`?  That satisfies both invariants. 
    1519 
    1620NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.