Hi Ender, The metamath-knife utility has the -F option to output Metamath's database formulas as s-expressions since version 0.3.9 <https://github.com/metamath/metamath-knife/releases/tag/v0.3.9> , which is a prefix format with parentheses.
Here is an example of outputs: ax-1: (wi wph (wi wps wph)) ax-2: (wi (wi wph (wi wps wch)) (wi (wi wph wps) (wi wph wch))) ax-3: (wi (wi (wn wph) (wn wps)) (wi wps wph)) mp2.1: wph mp2.2: wps mp2.3: (wi wph (wi wps wch)) areacirc: (wi (wa (wcel cR cr) (wbr cc0 cle cR)) (wceq (cfv carea cS) (co cpi cmul (co cR cexp c2)))) This option does not show which statements are hypotheses and which ones are theorem statements, but it would be easy to modify it to print different information. BR, _ Thierry -- 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 visit https://groups.google.com/d/msgid/metamath/aaf402a7-aa1f-4293-a06d-d7a344a1e967%40gmx.net.
