Frédéric Blanqui
Frédéric Blanqui
Right, -q doesn't print anything at all. I am not sure: perhaps it may be convenient to at least know which file is being checked. But there are other ways...
Hi. The short answer to your first question is: yes, unification rules are applied after decomposition and weak-head normalization. Is it a bug? Not really after the doc: "Given a...
If you print implicit arguments (flag "print_implicits" on) and the rules of set_cat_elim_func (print set_cat_elim_func), you see that the first rule actually is: rule @set_cat_elim_func $0 $1 (@set_cat_intro_func $2) ↪...
Did you try to install libev by hand (sudo apt-get install libev-dev)?
Could you please try with the branch nodream on [email protected]:fblanqui/lambdapi.git ?
For vscode, this is done now.
@01mf02 @gabrielhdt Do you have any idea about that? Which list of translators are you talking about?
> > Which list of translators are you talking about? > > https://github.com/Deducteam/lambdapi/blob/master/README.md You can make a PR.
Hi Amélie. This issue won't be solved any time soon, if any, as there is a simple work around: simply don't use prefix notations for non-unary symbols. Best regards, Frédéric.
> the Metamath to Lambdapi translator (which, by the way, is not mentioned in your list of translators). > > > Which list of translators are you talking about? >...