Coq - IP 表示法答案

【问题标题】：Coq - IP NotationCoq - IP 表示法
【发布时间】：2014-03-30 09:51:29
【问题描述】：

Coq - IP 表示法

我想为 IP 地址创建一个符号。以下是我的符号定义，可以正常工作：

Inductive IP := ip : nat -> nat -> nat -> nat -> IP.
Notation "a . b . c . d" := (ip a b c d) (at level 100).

但是当我尝试使用它时，

Definition ex := ( 192 . 168 . 1 . 1 ).

我收到以下错误：

Syntax error: [constr:operconstr level 200] expected after "." (in [constr:operconstr]).

我必须进行哪些更改才能修复此错误。

【问题讨论】：

我不是 100% 确定，但我认为您不能在符号中使用 ''.''。我尝试使用 Notation "(a 'foo' b 'foo' c 'foo' d )" := (ip a b c d) （在 100 级）。定义 ex := (192 foo 168 foo 1 foo 1)。（注意额外的括号）并且它有效，但与 ''.'' 相同也失败了。您可能必须声明一个新范围或其他内容。

标签： ip notation coq

【解决方案1】：

如果您可以从 ''.'' 切换到另一个符号，它应该可以工作（注意已经存在的符号并使用范围以确保安全）：

Inductive IP := ip : nat -> nat -> nat -> nat -> IP.
Notation "a * b * c * d" := (ip a b c d) (at level 100) : MY_scope.

Delimit Scope MY_scope with MY. 

Definition ex := ( 192 * 168 * 1 * 1 )%MY.

根据符号（例如使用 '','' 不能立即工作），您可能需要帮助解析器通过添加开始/结束标记：

(* without the ( and ) it fails *)
Notation "( a , b , c , d )" := (ip a b c d) (at level 100) : MY_scope.

Delimit Scope MY_scope with MY. 

Definition ex := ( 192 , 168 , 1 , 1 )%MY.

如果你真的想使用 ''.''，也许 Coq-Club 邮件列表上的某个人可以帮助你。

最好，五、

【讨论】：