I am working on my own verifier <https://github.com/mrakgr/Metamath-in-Fsharp> and am in the debugging stage. I can verify demo0.mm, but I've encountered a strange issue while trying to verify set.mm.
* dummylink $p |- ph $=* * ( ) C $.* I am not sure what *C* is here, but *(* and *)* should definitely be constants. This surprised me. I might have missed it while reading the manual, but I had not expected that constants could just be placed on the stack. Am I wrong here? -- 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/c8a819ea-edde-494d-8596-5b61612a1c75%40googlegroups.com.