Today we reviewed some of the equality eliminators of Pie, including cong, replace, symm, and trans, and gave implementations of cong, symm, and trans in terms of replace. We considered briefly the ind-= eliminator, which appears to offer additional power over replace, although we're currently at a bit of a loss as to how to use it.
Please read through Chapter 13 for next time.
No comments:
Post a Comment