EECS 755

Software Requirements Modeling and Analysis


Mystery tactics

I’ve used a few tactics in the Crypto.v theory that I did not discuss in class. You do not need to understand any of them to use the theory. If you’re curious, all of them are in the Coq definition and/or used in Pierce or Chlipala. Here’s a list of basic descriptions to get you started if you want to learn more:

You’ll also see significant usage of try and ; as presented in class. you don’t need to understand either one, but I did go through them briefly in class.