- 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 talked with a couple of student who are trying to use `Eval`

on theorems. Specifically:

`Eval compute in some_theorem.`

This will not help. You should be using `Eval`

with the functions you write for testing. `Eval`

applies the tactic `compute`

to its argument. If that is a function, then it evaluates the function as far as it can. For a theorem or lemma, there is nothing really that it can do. It will apply the tactic as you ask it to, but I don’t think the results will ever be useful.