Coq：錯誤：在當前環境中找不到參考_0

我是Coq新手。我在使用單位，產品和總和來定義列表，地圖和樹時遇到問題。我在標題中看到錯誤信息。評論上面的代碼工作正常，它下面的代碼沒有。Coq：錯誤：在當前環境中找不到參考_0

Inductive one : Type := nil : one. 

Inductive sum (t0 t1 : Type) : Type := 
    | inject_left : t0 -> sum t0 t1 
    | inject_right : t1 -> sum t0 t1. 

Inductive product (t0 t1 : Type) : Type := pair : t0 -> t1 -> product t0 t1. 

Definition list (t0 : Type) : Type := sum one (product t0 (list t0)). 

Definition map (t0 t1 : Type) : Type := list (product t0 t1). 

(* From here on nothing works. *) 

Definition List (t0 : Type) : Type := sum one (product t0 (List t0)). 

Definition map (t0 t1 : Type) : Type := 
    sum one (product (product t0 t1) (map t0 t1)). 

Definition Map (t0 t1 : Type) : Type := 
    sum one (product (product t0 t1) (Map t0 t1)). 

Definition tree (t0 : Type) : Type := 
    sum one (product t0 (product (tree t0) (tree t0))). 

Definition Tree (t0 : Type) : Type := 
    sum one (product t0 (product (Tree t0) (Tree t0))).

來源

2012-07-01 user1494846

回想起來，我猜測列表的定義只是因爲它已經隱式導入了。我想我需要使用_Inductive_來定義遞歸類型。 – user1494846

Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).

在勒柯克，您不能使用Definition寫一個遞歸函數，你需要使用Fixpoint（或更強烈的東西）。見http://coq.inria.fr/refman/Reference-Manual003.html#@command14

現在，這不是全部，但遞歸定義必須可證實終止（以確保您使用的邏輯的一致性）。既然你做你得到了在同樣的參數遞歸調用

Fixpoint List (t0 : Type) : Type := sum one (product t0 (List t0)).

這顯然無法終止：特別的，你可以不寫類似。

無論如何，定義類型，像這些，你應該寧願使用Inductive（和CoInductive），因爲你已經想通了。

來源

2012-07-02 05:24:19 Ptival

Coq：錯誤：在當前環境中找不到參考_0

回答

相關問題