Symbol with prime cannot be user-defined
Compilation of the following line fails with messages Symbol eval'err cannot be user-defined
.
Not sure if this is a bug or expected behaviour. Replacing test'err
with test'_err
resolves the problem.
lemma test'err: true