coq。訂購一對自然數

我想定義一個歸納數據類型來保存一對自然數。下面是我做了什麼coq。訂購一對自然數

Definition ordered_pair := (nat * nat) % type. 

    Inductive nat_pair(A B:nat):ordered_pair:= 
    |pair :ordered_pair->ordered_pair.

它產生異常

Anomaly: Uncaught exception Reduction.NotArity. Please report.

有誰知道嗎？

來源

2014-02-24 Pretty

這個歸納定義沒有意義。

您定義的類型ordered_pair已經是自然數對的類型。它被定義爲一對類型，適用於nat類型的參數，所以建立這樣一個對你可以這樣做：

Definition p : ordered_pair := (23, 42).

現在，如果你想定義一個「類似的」（而不是「相同」）電感式，語法是：

Inductive nat_pair : Set := 
| pair : nat -> nat -> nat_pair 
.

請注意，你不採取自然數作爲類型參數，而是構造包含兩個這樣的數字。

您似乎對歸納定義存在一些誤解，所以我建議您閱讀更多關於它們的內容。

來源

2014-02-24 08:18:10 Ptival

他所面臨的例外是因爲感應類型的arity（如果您不熟悉arity的概念，請讀取「type」）形式爲forall（x_1：A_1）（x_2：A_2）。（x_n：A_n），Prop'，'forall（x_1：A_1）（x_2：A_2）...（x_n：A_n），Set'或'forall（x_1：A_1）（x_2：A_2）... （x_n：A_n），類型'。這是完整的形式，通常它是非依賴的，只是形狀爲'A_1 - > ... - > A_n - > Prop'（等等）。在你的情況下，它是arity'nat - > nat - > ordered_pair'這是不允許的。 – Vinz

是的，Coq的新版本有一個稍微不太明顯的錯誤信息，但它仍然是關於arity，這可能會讓初學者感到困惑。基本思想是，你可以用歸納定義來豐富你的類型，它們是'Set'' Prop'和'Type'，而不是像'ordered_pair'這樣的用戶定義類型。但即使如此，對於似乎對歸納類型定義本身感到困惑的人來說，這似乎也是一個複雜的解釋。 – Ptival

coq。訂購一對自然數

回答

相關問題