Yes, using the metamath.exe program, MM> read set.mm MM> save proof * /normal MM> write source set.mm
The output file size will be very large, although I haven't checked its size recently. It will also be slower to read and verify. There are actually 6 formats recognized by metamath.exe (though only "compressed" and "normal" are official). These are discussed here: https://groups.google.com/d/msg/metamath/7uJBdCd9tbc/r5iRJifpAgAJ in case another format would be more useful for your project. Norm On Friday, October 18, 2019 at 1:17:08 PM UTC-4, Juho Kupiainen wrote: > > I would like to see the entire metamath database in uncompressed format. > Is there a way to do this? > -- 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/ceb4821e-d7d4-46ef-8759-5b50e848b1bf%40googlegroups.com.
