0

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.

这个定义的奇怪之处在于将andcoqdoc --html识别为两个单独的标记：EvalOp

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

为什么 Coq 允许在中间没有分隔符（空格）的两个标记？或者这是一个错误coqdoc？感谢您的帮助！

4

1 回答 1

3

为什么 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 的解析器玩这样的游戏。

于 2018-05-10T00:50:04.793 回答