I’ve recently tested how well PVS handles Japanese. I was pleased to see that in general it handles it well. However, one surprise I encountered was in the following bit of PVS code:
真(p_しません: bool): bool =
しません(p_偽: bool): bool =
When I try to parse the theory, I get “Found '±' when expecting ')’” when it encounters the first “ん”. If I change that line and the line below it to use “n” instead of “ん”, I then get the error “Found '!id!' when expecting 'END’” for the second function. If I then also replace that “ん” with “n”, then the theory parses fine. My current work around is to simple perform that replacement (since “n” is actually pretty close to “ん”).
Is this a known issue, and is there any fix in the works? This is not a high-priority issue for me, but I thought I’d bring it to your attention in case it’s not already known.