Changes between Version 13 and Version 14 of TypeFunctionsSolving


Ignore:
Timestamp:
Jul 30, 2008 3:14:47 PM (7 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.