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 validdk
identifiers or that aredk
keywords are enclosed between{|
and|}
.In module names, dots are replaced by underscores and, if a
lp
file requires the modulemylib.logic.untyped.fol
, its translation will require the filemylib_logic_untyped_fol.dk
. Therefore, in a package whoseroot_path
ismylib.logic
, the fileuntyped/fol.lp
is translated intomylib_logic_untyped_fol.dk
.