Missing keywords

[fblanqui]

Hi Michael. Would it be possible to accept the keywords "#REQUIRE" and "injective", even if you do nothing with them? This would help using kocheck with currently produced dk files without having to modify them beforehand.

[01mf02]

Hi Frédéric, I have done the first part, namely to parse pragmas, including #REQUIRE, in 83c394a.

Regarding injective, I was thinking about supporting private at the same time. However, I am currently having trouble to recall the details of the syntax of the Dedukti standard. Can you enlighten me which of the following commands are correct?

1. private def a: b.
2. private def a := b.
3. private thm a: b := c.

(I have the impression that the standard rules out all of those, but I do not recall why ...)

[fblanqui]

I think that only 1 makes really sense as declaring a as private allows to pattern match on a but not use a directly. Private symbols are constant (have no definition) usually.