Compatibility with Dedukti

Lambdapi can read Dedukti files with the extension .dk, and translate Lambdapi files to Dedukti files, and vice versa, by using the export command.

Moreover, a Lambdapi file can refer to a symbol declared in a Dedukti file.

In case there are two files file.dk and file.lp, file.lp is used.

Remarks on the export to Dedukti:

When a lp identifier or module/file name is not a valid dk identifier or module/file name (the lp and dk formats do not accept the same class of identifiers and module/file names), we try to rename them instead of failing:

• lp identifiers that are not valid dk identifiers or that are dk keywords are enclosed between {| and |}.

• In module names, dots are replaced by underscores and, if a lp file requires the module mylib.logic.untyped.fol, its translation will require the file mylib_logic_untyped_fol.dk. Therefore, in a package whose root_path is mylib.logic, the file untyped/fol.lp is translated into mylib_logic_untyped_fol.dk.