mathlib
e7a4b12c - fix(tactic/core): fix infinite loop in emit_code_here (#4746)

Commit
5 years ago
fix(tactic/core): fix infinite loop in emit_code_here (#4746) Previously `emit_code_here "\n"` would go into an infinite loop because the `command_like` parser consumes nothing, but the string is not yet empty. Now we recurse on the length of the string to ensure termination. Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Author
Parents
Loading