This happened in Johannes' real number formalization. We tried to unfold a noncomputable definition even though it would have been erased afterwards, and failed. The check_computable check was introduced in order to fix the error message in #1401, the error message is still intelligible in that example. |
||
|---|---|---|
| .. | ||
| lean | ||
| .gitignore | ||