When a proof is started with begin but end is missing at the end of the proof (whether the proof is completed or not), Both the Lambdapi command line and Lsp show the message Unexpected token: "". while it should be end missing.
For instance, with the following file
verbose 3;
constant symbol T : TYPE;
opaque symbol trivial : T → T → T → T
≔ begin
The command line check command produces :
Checking "somefile.lp" ...
verbose 3
somefile.lp:2:0-25
symbol T : TYPE
[somefile.lp:5:7] Unexpected token: "".
Moreover, in Vscode (and probably with Emacs too), the console doesn't show the log messages (despite console 3; at the beginning of the file) except the last one which is Unexpected token: "".
When a proof is started with
beginbutendis missing at the end of the proof (whether the proof is completed or not), Both the Lambdapi command line and Lsp show the messageUnexpected token: "".while it should beend missing. For instance, with the following fileThe command line check command produces :
Moreover, in Vscode (and probably with Emacs too), the console doesn't show the log messages (
despite console 3;at the beginning of the file) except the last one which isUnexpected token: "".