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.