- Project 3 Extension
- Mystery tactics
- Crypto theory
- Project 3 is posted
- Runtime Checks to Type Checks
- Dependent Register File
- Bounded register file
- Array model from class
- distr_rev
- Eval on theorems

Blog

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:

`exists`

- like intro, but for existential quantifiers.`tauto`

- a tautology solver. Like omega, but for propositional logic statements.`refine`

- tell Coq to set up and attempt proofs that fill in holes (i.e.`_`

) in the associated definition.

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.