Что такое EvalOp в Coq CompCert

Question

Определение EvalOp находится в compcert.backend.SplitLongproof:

Ltac EvalOp :=
  eauto;
  match goal with
  | [ |- eval_exprlist _ _ _ _ _ Enil _ ] => constructor
  | [ |- eval_exprlist _ _ _ _ _ (_:::_) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (Eletvar _) _ ] => constructor; simpl; eauto
  | [ |- eval_expr _ _ _ _ _ (Elet _ _) _ ] => econstructor; EvalOp
  | [ |- eval_expr _ _ _ _ _ (lift _) _ ] => apply eval_lift; EvalOp
  | [ |- eval_expr _ _ _ _ _ _ _ ] => eapply eval_Eop; [EvalOp | simpl; eauto]
  | _ => idtac
  end.

Что странного в этом определении? coqdoc --html признать Eval а также Op как два отдельных токена:

<span class="id" title="keyword">Eval</span><span class="id" title="var">Op</span>

Почему Coq допускает два токена без разделителей (пробелов) в середине? Или это ошибка coqdoc? Спасибо за помощь!

Answer 1

Почему Coq допускает два токена без разделителей (пробелов) в середине? Или это ошибка coqdoc?

Это ошибка coqdoc, Coq не допускает двух алфавитных токенов без буквенно-цифровых символов между ними, но есть много других примеров токенов без разделителей. Например, это допустимый Coq:

Definition(*no-spaces*)foo:=1.

Это лексируется как токены Definition, комментарий (*no-spaces*), foo, :=, 1, а также ., Я верю. Вы также можете играть в глупые игры с числовыми токенами, например,

Coercion Nat.add:nat>->Funclass.
Axiom a:nat.
Check 1a:nat.

Поскольку идентификаторы не могут начинаться с цифр, Coq анализирует 1a как 1 применительно к a, который проверяет тип из-за Coercion, Вы, вероятно, не должны играть в такие игры с парсером Coq.