Error when '.,' appears in disjoints

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).

https://expln.github.io/lamp/latest/index.html

MIT License

12 stars 5 forks source link

Error when '.,' appears in disjoints #199

Open BTernaryTau opened 1 month ago

BTernaryTau commented 1 month ago

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."

zwang123 commented 3 weeks ago

Same happened here for .+ and .<_ in prdsval.