正在访问agda中Stream中的元素

Question

我制作了一个（N x N）类型的流。如何访问该对中的单个元素？？

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

它说流中没有构造函数，。我心中有一个解决方案，我将创建成对的记录，然后它就会起作用。除此之外，还有任何其他方法可以访问元素。

Answer 1

构造函数是_∷_（键入::以获得∷），而不是_::_。

无论如何，你的定义是无效的，也不能说服终止检查器。