Error when '.,' appears in disjoints
Closed this issue · 6 comments
If a theorem has a variable with the name '.,' in a distinct variable group (such as ipffval), mm-lamp incorrectly interprets the comma as separating two variables and gives the error "The symbol '.' is not a variable but it is used in a disjoint statement."
Same happened here for .+ and .<_ in prdsval.
Thank you for reporting this bug. It is fixed in the dev version of mm-lamp. The fix was to use spaces instead of commas as delimiters for variables in distinct variable groups. This however introduced a small breaking change. You'll have to manually replace commas with spaces in your active proof in mm-lamp in dev version.
Does this also apply to proofs imported from JSON or are those converted automatically when they are loaded?
Yes, it also applies to proofs imported from JSON. To be honest I forgot about this use case. Looks like it is a problem if somebody stored a lot of proofs in the form of URL (which uses the same mechanism as importing from JSON). I will check if I can implement the automatic conversion. Thanks for reminding me about that use case.
The automatic conversion has been implemented in the dev version. It works for all cases: importing from old JSONs, opening old URLs, switching from the old mm-lamp version to the dev one.
The fix is available in version 25.