Coq CompCert中的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的一个bug？谢谢你的帮助！

Answer 1

为什么Coq允许中间没有分隔符(空格)的两个令牌？或者这是coqdoc的一个bug？

这是coqdoc的一个bug。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的解析器中玩这种游戏。