Frédéric Blanqui
Frédéric Blanqui
Lambdapi emits a warning if it detects that the LHS cannot be typable. It cannot emit a warning each time it finds out that a LHS is typable only under...
@rlepigre : would you have time to take care of this issue?
I disagree. Identifiers should be different from keywords. But there is no reason to do this for module names since they are not first-class objects and are used to qualify...
But I guess that an editor can easily distinguish in a qualified identifier the path part from the name part.
It occurs after "as".
Hello @nathancarter . I didn't try myself but @ejgallego did it for Coq and it worked very well (see https://github.com/jscoq/jscoq), and I would be very interested to have lambdapi run...
Now, for your example, you can also simply do: ``` assume a b f fa ab; rewrite left ab; apply fa; ``` But I agree that it could sometimes be...
Are you sure about 423? sign.ml has less lines.
The assert false is line 340.
Right, we could add some error message before assert false saying that some lpo file is maybe out of date, but we should keep the assert false, don't you think...