The library defines an abstract syntax tree in lib/ast.ml for STTfa terms.
The first step of the process is to translate Dedukti files in the encoding of
STTfa to abstract syntax trees. Then for any system S available (they are
defined in lib/systems.mli), an exporter can be obtained using
Systems.exporter S. Such an exporter is a module with a function print_ast.
The code has been extracted from logipedia.
If you want to add a new exporter:
- Write a new module that implements the interface
Sttfaxport.EXP - Add a new constructor in the type
Sttfaxport.system - Extend the function
Sttfaxport.exporterfrom the new constructor to the new module