Closed wlammen closed 1 year ago
By the way: should you add mmfatl.c to the following list at the beginning of metamath.c:
/* The overall functionality of the modules is as follows:
metamath.c - Contains main(); executes or calls commands
mmcmdl.c - Command line interpreter
mmcmds.c - Extends metamath.c command() to execute SHOW and other
commands; added after command() became too bloated (still is:)
mmdata.c - Defines global data structures and manipulates arrays
with functions similar to BASIC string functions;
memory management; converts between proof formats
mmhlpa.c - The help file, part 1.
mmhlpb.c - The help file, part 2.
mminou.c - Basic input and output interface
mmpars.c - Parses the source file
mmpfas.c - Proof Assistant
mmunif.c - Unification algorithm for Proof Assistant
mmveri.c - Proof verifier for source file
mmvstr.c - BASIC-like string functions
mmwtex.c - LaTeX/HTML source generation
mmword.c - File revision utility (for TOOLS> UPDATE) (not generally useful)
*/
?
@digama0 ready to merge