Changes between Version 15 and Version 16 of TypeFunctionsSynTC
 Timestamp:
 Dec 12, 2006 8:34:02 PM (9 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeFunctionsSynTC
v15 v16 481 481 Normalisation of an equality `s = t` of arbitrary type terms `s` and `t` (not containing schema variables) leads to a (possibly empty) set of normal equations, or to a type error. We proceed as follows: 482 482 483 1. Reduce `s` and `t` to HNF, giving us `s'` and `t'`.483 1. Reduce `s` and `t` to NF, giving us `s'` and `t'`. 484 484 2. If `s'` and `t'` are the same variable, we succeed (with no new rule). 485 485 3. If `s'` or `t'` is a rigid variable, we fail. (Reason: cannot instantiate rigid variables.)