Dedukti icon indicating copy to clipboard operation
Dedukti copied to clipboard

Fix #295

Open GuillaumeGen opened this issue 5 months ago • 1 comments

This is the simplest fix to #295 . Consequence of this fix is that now, if one names a module with a keyword, they have to require it using "{|...|}". This seems to be a very sensible constraint to me, but it is a non-backward compatible change.

There is another possibility, to avoid this change, which is to duplicate the system we created for ident with the sident and buffering but for mident, so to have a smident so to say. If backward compatibility is crucial (ie more important than avoiding code duplication for maintainability), then I can implement the other proposed solution, it is quite simple too.

GuillaumeGen avatar Mar 01 '24 17:03 GuillaumeGen