Dedukti icon indicating copy to clipboard operation
Dedukti copied to clipboard

Published 20 hours ago • verified publisher icon Deducteam

Typo in documentation

Open gabrielhdt opened this issue 3 years ago • 5 comments

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

gabrielhdt avatar Dec 20 '21 14:12 gabrielhdt

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).

fblanqui avatar Dec 20 '21 17:12 fblanqui

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

gabrielhdt avatar Dec 20 '21 20:12 gabrielhdt

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

gabrielhdt avatar Dec 20 '21 20:12 gabrielhdt

But is this file automatically generated from the grammar?

fblanqui avatar Dec 21 '21 08:12 fblanqui

Yes it is https://github.com/Deducteam/Dedukti/blob/c65e7e66fe4bb8285db1856b8fe2a2532da2bd50/Makefile#L165

gabrielhdt avatar Dec 21 '21 08:12 gabrielhdt