EECS 755

Software Requirements Modeling and Analysis


Eval on theorems

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.