To make Dedukti compliant with the standard, we add two options:
--explicit-import
--standard
which are deactivated by default. For the moment, the second option is an alias of the first one.
The reason why it is deactivated by default is to prevent many generated dedukti files to not type check anymore. The associated makefiles need to be updated consequently.
To make Dedukti compliant with the standard, we add two options:
--explicit-import--standardwhich are deactivated by default. For the moment, the second option is an alias of the first one.
The reason why it is deactivated by default is to prevent many generated dedukti files to not type check anymore. The associated makefiles need to be updated consequently.