Hi Savask,
For syntax check you also can use mm-lamp. You have to put each statement one by one into mm-lamp, so this is not very convenient, but it doesn’t require any installation. 1. Navigate to the mm-lamp web site https://expln.github.io/lamp/latest/index.html 2. In the “Source type” select “Web” 3. In the “Alias” select “set.mm:latest” 4. In the opened confirmation dialog click “Confirm”. This will start downloading the latest version of set.mm from us.metamath.org. Wait until the file is loaded (for me it takes about 20 seconds) 5. In “Scope” select “Stop before” 6. In “Label” type “box” and select “mathbox” from the dropdown 7. Click “Apply Changes” 8. Add all the statements you want to check by clicking “+” button. You may see letters G and P appear to the left of each statement. They don’t matter for syntax checking. 9. Click “Unify all” button. This button has shape of a few small connected circles. Make sure all the statements you’ve added are unselected before clicking this button (the checkbox to the left of each statement is empty). 10. If any of the statements have syntax error, you will see an error message in red color under such statement. I checked all the statements from your challenge - all of them are syntactically correct. Nice challenge by the way, I will be happy to spend some time on it. – Igor On Sunday, December 10, 2023 at 7:02:11 PM UTC+1 Glauco wrote: > 1. When preparing the challenge, I was wondering if I missed a bracket > somewhere or forgot to put some brackets etc. Is there an easy way to check > that a statement passes grammar checks? I think mmj2 could do that, but it > is rather cumbersome to use as it is not really supported anymore. > > > Hi Savask, > > Yamma checks the grammar of every line of a .mmp file > > It gives you a Diagnostic at the first symbol that does violate the > grammar (and it suggests you all possible valid characters, at that point > of the line) > > But I believe that Yamma is at least as cumbersome as mmj2 :-) > > > > > -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/570738ae-db04-431f-98db-020bf2910391n%40googlegroups.com.
