我嘗試學習 agda 并使用教程。我粘貼兩個相互遞回集的代碼
module MoreSets where
data List? (A B : Set) : Set
data List? (A B : Set) : Set
data List? (A B : Set) where
[] : List? A B
_∷_ : A → List? A B → List? A B
data List? (A B : Set) where
_∷_ : B → List? A B → List? A B
并得到錯誤
MoreSets.agda:6,12-23
Unexpected type signature for parameters A B
when checking the definition of List?
我假設有一個微不足道的錯誤，但看不到它。
對于不深入范疇論的 Haskell 程式員來說，學習 agda 的簡單教程是什么？
uj5u.com熱心網友回復：
在定義歸納型別時，您不應該重復宣告中的型別注釋。所以：
module MoreSets where
data List? (A B : Set) : Set
data List? (A B : Set) : Set
data List? A B where
[] : List? A B
_∷_ : A → List? A B → List? A B
data List? A B where
_∷_ : B → List? A B → List? A B
轉載請註明出處，本文鏈接：https://www.uj5u.com/net/536817.html
標籤：阿格达