Uncompressed proofs

[Andrew Thompson Thompson]

Hi,

I'm working on a verifier and didn't want to implement the compressed notation initially.  What is the easiest way to get set.mm in uncompressed form ? 

Iv'e tried playing with the metamath program but it doesn't want to do it for me...

Kind regards

Andrew

[Discher, Samiro]

"but it doesn't want to do it for me"

Not sure what your issue is, but according to some of my old notes about how to use metamath.exe:

read set.mm
save proof * /fast /packed
write source set_fast_packed.mm
save proof * /explicit
write source set_explicit.mm
save proof * /normal
write source set_normal.mm

I suppose you want the first and the last line. These have to be entered after starting metamath.exe (so that "MM> " is displayed in your console).

---

Von: 'Andrew Thompson Thompson' via Metamath <meta...@googlegroups.com>
Gesendet: Sonntag, 14. April 2024 22:42:22
An: Metamath
Betreff: [Metamath] Uncompressed 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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/55b14eda-5f30-44a5-b829-67345517f606n%40googlegroups.com.