Class CoqExporter

java.lang.Object

org.episteme.core.mathematics.loaders.logic.CoqExporter

All Implemented Interfaces:

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

public class CoqExporter
extends Object
implements FormalSystemExporter

Exporter for the Coq Proof Assistant.

Generates Coq vernacular (.v) files.

Since:

1.0

Author:

Silvere Martin-Michiellot, Gemini AI (Google DeepMind)

Constructor Summary

Constructors

Constructor	Description
CoqExporter()

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

CoqExporter

public CoqExporter()

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")