Changes between Version 13 and Version 14 of TypeFunctionsSolving
 Timestamp:
 Jul 30, 2008 3:14:47 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSolving
v13 v14 13 13 14 14 The types `t`, `t1`, ..., `tn` may not contain any occurrences of synonym families. Moreover, in Forms (2) & (3), the left and righthand side need to be different, and the lefthand side may not occur in the righthand 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 newsingle.tex. But they don't line up exactly. For example, what about `F [x] ~ G x`? That satisfies both invariants. 15 19 16 20 NB: We explicitly permit equalities of the form `x ~ y` and `a ~ b`, where both sides are either flexible or rigid type variables.