Class MetamathExporter

java.lang.Object

org.episteme.core.mathematics.loaders.logic.MetamathExporter

All Implemented Interfaces:

ResourceIO<Map<String,Object>>, ResourceWriter<Map<String,Object>>, FormalSystemExporter

public class MetamathExporter
extends Object
implements FormalSystemExporter

Exporter for Metamath.

Generates Metamath database (.mm) files.

Since:

1.0

Author:

Silvere Martin-Michiellot, Gemini AI (Google DeepMind)

Constructor Summary

Constructors

Constructor	Description
MetamathExporter()

Method Summary

Modifier and Type	Method	Description
void	exportSystem(Map<String,Object> system, Writer writer)	Exports the given logical context/system to the specified writer.
String	getFileExtension()	Returns the file extension typically used by this system.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface FormalSystemExporter

exportSystem, exportSystem, getCategory, getDescription, getLongDescription, getName, getResourcePath, getResourceType, getSupportedVersions, save

Methods inherited from interface ResourceIO

getExpectedResourceFiles, getSupportedExtensions, isFileBased, isInput

Methods inherited from interface ResourceWriter

isOutput

Constructor Details

MetamathExporter

public MetamathExporter()

Method Details

exportSystem

public void exportSystem(Map<String,Object> system,
 Writer writer)
                  throws IOException

Description copied from interface: FormalSystemExporter

Exports the given logical context/system to the specified writer.

Specified by:

exportSystem in interface FormalSystemExporter

Parameters:

system - the system components to export

writer - the writer to output to

Throws:

IOException - if an I/O error occurs

getFileExtension

public String getFileExtension()

Description copied from interface: FormalSystemExporter

Returns the file extension typically used by this system.

Specified by:

getFileExtension in interface FormalSystemExporter

Returns:

the file extension (e.g., ".v", ".mm")