| exceptionalTrace.lean:7:0-7:13: error: maximum recursion depth has been reached | |
| use `set_option maxRecDepth <num>` to increase limit | |
| use `set_option diagnostics true` to get diagnostic information | |
| [Elab.step] expected type: <not-available>, term | |
| rt + 1 | |
| [Elab.step] expected type: <not-available>, term | |
| binop% HAdd.hAdd✝ rt 1 | |
| [Elab.step] expected type: <not-available>, term rt |