New syntax for pragmas and assertions

[dwarfmaster]

Implement the new syntax for pragmas and assertions as discussed.

[gabrielhdt]

All right, I'll just inline some example file here to have a taste of it

(; OK ;)

A : Type.
def B := A.
def C := A.
D : Type.

assert |- B == A.
assert |- B == C.
(;# assertnot A == D #;)

[dwarfmaster]

All previous pragmas of the form #PRAGMA... are still supported as (;# PRAGMA ... #;), making it easy to update tests.

[GuillaumeGen]

This syntax change requires an update of the syntax.bnf file (generated by a command like make bnf) and of the README (at least the "Commands" section, probably some other occurrences too).

[francoisthire]

Why not call it infer?

[gabrielhdt]

I think it's because it is an assertion, so we are thinking of a predicate rather than a computation. In particular, the Dedukti command Typeable(c, t) should not print anything. It could be IsTypeable, if you want to stress out the predicate.