Coq CompCert 中的 EvalOp 是什么

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

Why would Coq allow two tokens with no separators (spaces) in the middle? Or is this a bug of 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 的解析器玩这样的游戏。

Coq CompCert 中的 EvalOp 是什么

What is the EvalOp in Coq CompCert

coq

coq-tactic

compcert

coq-extraction