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 

Reply via email to