Какие зарезервированные ключевые слова в Coq? - PullRequest
Новая
       10

Какие зарезервированные ключевые слова в Coq?

2 голосов
/ 03 мая 2019

Я хотел бы иметь список всех ключевых слов в Coq, которые нельзя использовать в качестве имен идентификаторов.

https://coq.inria.fr/refman/language/gallina-specification-language.html#lexical-conventions предоставляет список ключевых слов, которые зарезервированы в Галлине, но не включает ключевое слово «по».

Тем не менее, Definition by:=O не компилируется и выдает ошибку Syntax error: [Prim.ident_decl] expected after [def_token] (in [vernac:gallina]).. Это указывает на то, что приведенный выше список ключевых слов не является полным, поэтому, если у кого-то есть полный список, я был бы очень признателен.

1 Ответ

0 голосов
/ 03 мая 2019

Это говорит о том, что Coq использует by в качестве (истинного) ключевого слова с 8.3.

Похоже, что плагин Ltac делает соответствующее объявление здесь , потому что если мы отключим плагин, то by можно будет использовать снова: 

coqtop -noinit
Welcome to Coq 8.9.0 (April 2019)

Coq < Inductive T := t.
T is defined
T_rect is defined
T_ind is defined
T_rec is defined

Coq < Definition by := t.
by is defined
...