[Metamath] Is it possible for a constant to become inactive?

As the language is simple enough, I've decided to try implementing it on my own in F# in order to get a grasp on it. In the spec (page 132/247 of the Metamath book) it says that constants can only be declared in the outermost block, so I am wondering how it would be possible for them to become

[Metamath] How to process dummylink?

I am working on my own verifier 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 *)*

[Metamath] Re: How to process dummylink?

Sorry about this, as soon as I posted I realized that I had completely forgotten about compressed proofs. -- 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+u

[Metamath] Re: How to process dummylink?

Well, at any rate as I've been working on this for 9 days now I'll stop here. I do not feel like going those last few extra miles just to implement proof decompression and test it thoroughly on the big library. I am not sure how stringent the criteria for inclusion on that list of verifiers in

Re: [Metamath] Re: How to process dummylink?

d here > > https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ > > Can your verifier check demo0.mm yet? ( > https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm) > > Best regards, > > Antony > > > On Tue, Dec 3, 2019 at