Coq-IP表示法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]).
我有什麼要改變來解決這個錯誤。 '。「
如果你可以從」切換到另一種符號，它應該工作（照顧已經存在的符號和使用範圍的是安全的）：
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俱樂部郵件列表可以幫助你。
最佳， 五
我不是100％肯定，但我不認爲你可以使用「」「」的符號。我試過 符號「（a'foo'b'foo'c'foo'd）」：=（ip a b c d）（等級100）。 定義ex：=（192 foo 168 foo 1 foo 1）。 （注意附加括號），它的工作原理，但與''。''相同也失敗。你可能需要聲明一個新的範圍或其他東西。 – Vinz