New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Typo in documentation #255

Open

gabrielhdt opened this issue Dec 20, 2021 · 5 comments

Member

gabrielhdt commented Dec 20, 2021 •

edited

Loading

The README.md states that injectivity is enabled with inj (https://github.com/Deducteam/Dedukti#injectivity), but it is enabled with injectivity

The text was updated successfully, but these errors were encountered:

Member

fblanqui commented Dec 20, 2021

It could be useful to include https://github.com/Deducteam/lambdapi/blob/master/docs/syntax_dedukti.bnf in Dedukti (this grammar is generated in https://github.com/Deducteam/lambdapi/blob/master/docs/Makefile).

Member Author

gabrielhdt commented Dec 20, 2021

It is already at the root of the repository https://github.com/Deducteam/Dedukti/blob/master/syntax.bnf

Member Author

gabrielhdt commented Dec 20, 2021

It looks out of date, there is no mention of injective.

Member

fblanqui commented Dec 21, 2021

But is this file automatically generated from the grammar?

Member Author

gabrielhdt commented Dec 21, 2021

Yes it is

Dedukti/Makefile

Line 165 in c65e7e6

bnf:

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment