The go_string parsing ideally should handle escape sequences the same way Go does (https://go.dev/blog/strings describes this). Single escape cases are straightforward to parse, but handling multiple escapes seems to be harder because there are more branches to handle which puts pressure on rocq's recursion handling when trying to prove lemmas.
The go_string parsing ideally should handle escape sequences the same way Go does (https://go.dev/blog/strings describes this). Single escape cases are straightforward to parse, but handling multiple escapes seems to be harder because there are more branches to handle which puts pressure on rocq's recursion handling when trying to prove lemmas.