Changes between Version 86 and Version 87 of TypeFunctionsSolving


Ignore:
Timestamp:
Sep 7, 2008 5:38:34 AM (6 years ago)
Author:
chak
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeFunctionsSolving

    v86 v87  
    242242 1.  '''Substitution:''' For any variable equality of the form `co :: x ~ t` (both local and wanted), we apply the substitution `[t/x]` to all equalities. 
    243243 2. '''Instantiation:''' For any variable equality of the form `co :: alpha ~ t` or `co :: a ~ alpha`, where `co` is wanted, we instantiate `alpha` with `t` or `a`, respectively, and set `co := id`. 
    244  
     244The substitution step can lead to recursive equalities; i.e., we need to apply an occurs check. 
    245245 
    246246== Examples ==