Coq中的新範圍

我想我自己的範圍，玩弄長長的分歧。Coq中的新範圍

Declare Scope my_scope. 
Delimit Scope my_scope with my. 
Open Scope my_scope. 

Definition f (x y a b : nat) : nat := x+y+a+b. 
Notation "x < y * a = b" := (f x y a b) 
(at level 100, no associativity) : my_scope. 

Check (1 < 2 * 3 = 4)%my.

你如何制定一個新的範圍？

編輯：我選擇了「x < y * a = b」來覆蓋Coq的運算符（每個運算符都有不同的優先級）。

來源

2013-02-23 sam boosalis

我不明白這個問題。你不是隻是自己的範圍？你怎麼沒有想要的？ – Gilles 2013-02-24 20:20:15

命令Declare Scope不存在。有關示波器的各種命令在section 12.2 of the Coq manual中描述。

您對示例符號的選擇存在固有問題，因爲它與預先定義的符號衝突，這似乎是在符號之前使用的符號。

當解析器看到_ < _，認爲你實際上是在談論整數比較第一成分看，那麼它看到第二部分作爲符號_ * _的一個實例，然後它會看到所有的左側平等的一面。而一直以來解析器是快樂的，它構造形式的表達式：

(1 < (2 * 3)) = 4

這是由解析器構造和類型系統尚未徵求。類型檢查器看到一個自然數作爲(_ < _)的第一個孩子，並且很高興。它認爲(_ * _)是第二個孩子，它很高興，現在知道該產品的第一個孩子應該是一個自然數，它仍然是幸福的;最後它具有相等性，並且這種相等性的第一個組成部分是Prop，但第二個組成部分的類型是nat。

如果您鍵入Locate "_ < _ * _ = _".答案會告訴您您確實定義了新的符號。問題是這個符號永遠不會被使用，因爲解析器總是找到它以前可以使用的另一個符號。理解爲什麼表示法比另一種更喜歡錶達式，需要更多的解析技術知識，正如Coq手冊第12章中的句子（我不明白）所暗示的那樣：

Coq可擴展解析由Camlp5執行， LL1解析器。

你必須選擇不同的變量，x，y，a，並且b的水平，使沒有這些變量都將能夠匹配太多的文本。例如，我嘗試定義一個符號靠近你的符號，但是有一個開始和結束括號（我想這大大簡化了任務）。的x水平被選擇爲比=水平下

Notation "<< x < y * a = b >>" := (f x y a b) 
(x at level 59, y at level 39, a at level 59) : my_scope.

，Y的電平被選擇爲比的*的電平低，的a水平被選擇爲比=低。通過閱讀命令Print Grammar constr.的答案獲得這些水平。它似乎正常工作，因爲接受了以下命令。

Check << 1 < 2 * 3 = 4 >>.

但是，您可能需要包括更多的工程，纔能有一個非常好的符號。

來源

2013-02-25 23:08:00 Yves

我確實希望我愚蠢的4元操作員能夠影響coq's。沒有辦法減少包圍？「<< x >」表示「最左邊的非終端級別無法更改」。這是否與「本質上是LL1解析器」有關？ – 2013-02-28 05:41:19

要回答這個問題，實際在您的標題：當你聲明一個使用它的符號

新的範圍被創建。也就是說，您不要單獨聲明新的範圍my_scope。你只寫

Notation "x <<< y" := (f x y) (at level 100, no associativity) : my_scope.

，並聲明新的範圍my_scope。

來源

2014-12-06 15:13:19 PLL

Coq中的新範圍

回答

相關問題