207 | | applySubstFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- return only... |

208 | | applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...the modified... |

209 | | applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...equality |

210 | | |

| 207 | applySubstFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- return second argument... |

| 208 | applySubstVarVar :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...if it needs to go into... |

| 209 | applySubstVarFam :: RewriteInst -> RewriteInst -> Maybe EqInst -- ...the todo list |

| 210 | }}} |

| 211 | For `applySubstFam`, `applySubstVarVar`, and `applySubstVarFam`, if the rule is not applicable to the arguments in the given order, ''but it is applicable in the opposite order,'' return the second argument as if it had been modified. (As a result, it will get onto the todo list, and the equalities eventually be used in the opposite order.) |

| 212 | |

| 213 | The following function gets a list with all local and wanted equalities. It returns a list of residual equalities that permit no further rule application. |

| 214 | {{{ |

230 | | | Just eq2' <- applySubstFam eq1 eq2 = (norm eq2', []) |

231 | | | Just eq2' <- applySubstVarVar e1 eq2 = (norm eq2', []) |

232 | | | Just eq2' <- applySubstVarFam eq1 eq2 = ([eq2'], []) |

233 | | | otherwise = ([], [eq2]) |

| 234 | | Just eq2' <- applySubstFam eq1 eq2 = (norm eq2', [eq1]) |

| 235 | | Just eq2' <- applySubstVarVar e1 eq2 = (norm eq2', [eq1]) |

| 236 | | Just eq2' <- applySubstVarFam eq1 eq2 = ([eq2'], [eq1]) |

| 237 | | otherwise = ([], [eq1, eq2]) |