從agda訪問流中的元素

我做了一個（N×N）類型的流。我怎樣才能訪問這對單獨的元素？從agda訪問流中的元素

genL : ℕ → Stream (ℕ × ℕ) → Stream (ℕ × ℕ) 
genL k ((x , y) :: xs) = if ((y * k) lt x) then (x , y) :: (♯ genL k (♭ xs)) 
          else genL k (♭ xs)

它說沒有constuctor ，在流。我有一個解決方案，我會創建一對記錄，然後它會起作用。除此之外，還有沒有其他辦法可以使這一要素得到滿足。

來源

2015-03-31 ajayv

您是否在尋找[查詢]（http://agda.github.io/agda-stdlib/Data.Stream.html#2055）？如果沒有，你可以從寫你正在尋找的函數的類型開始嗎？ – gallais 2015-03-31 16:41:55

不，流的元素形式爲（x，y）。我想單獨訪問x和y。在代碼中，第二行不起作用。 – ajayv 2015-03-31 17:17:31

您可以使用Data.Product的爲[預測]（http://agda.github.io/agda-stdlib/Data.Product.html#525）。 – gallais 2015-03-31 17:23:44

構造函數是_∷_（類型\::得到∷），而不是_::_。

反正你的定義是不生產，不說服終止檢查。

來源

2015-04-01 06:24:45 user3237465

問題不在於「，」。這是錯字，即（：:)。如何說服終止檢查器？這是我放置NO_TERMINATION_CHECK的原因。 – ajayv 2015-04-02 06:13:37

@ajayv，目前尚不清楚你想達到什麼目的。有大約在CPDT書coinduction一個[章]（http://adam.chlipala.net/cpdt/html/Coinductive.html）。 – user3237465 2015-04-02 08:32:02

從agda訪問流中的元素

回答

相關問題