Is there a full documentation of Coq's grammar?

I could explain why it’s useful to have such complicated grammar but the question of “why” should rather be answered by people that were there in the beginnings of Coq. But for instance, the very powerful notation system is generally considered to be an ingredient of the success of Coq.

If you are planning to rely on SerAPI, then it is best that you let SerAPI do the splitting into sentences for you (this is something that it supports). Splitting sentences based on . is an approximation that works relatively well but there will be edge cases. An example (which I didn’t invent) is the following:

Notation "( a . b )" := (a, b).
Check (1 . 2).

It is an extreme example because most IDEs (including CoqIDE) won’t accept it (because they try to do the sentence splitting by themselves but are not aware of the notation system) but coqc will. And yet, the sentence splitting code in CoqIDE is already quite complex (cf. https://github.com/coq/coq/blob/51ecccef0308eceec1ddd9776a03fd993b3ea71a/ide/coqide/coq_lex.mll#L102-L154).

2 Likes