As documented in https://lambdapi.readthedocs.io/en/latest/module.html, a lambdapi.pkg must be placed at the root of the source tree of a library under development. When used with the command line, the absence of this file rises an error. However, when used with editors (both Vscode and Emacs), no error is displayed.
fblanqui
commented
5 months ago
As documented in https://lambdapi.readthedocs.io/en/latest/module.html, a lambdapi.pkg must be placed at the root of the source tree of a library under development. When used with the command line, the absence of this file rises an error. However, when used with editors (both Vscode and Emacs), no error is displayed.
This PR fixes #1069