在Agda中访问Stream中的元素 [英] Accessing element from Stream in agda

问题描述

我做了一个（N×N）类型的流。我怎样才能访问这对单个元素？

  genL：ℕ→流（ℕ×ℕ）→流（ℕ （x，y）:: xs）= if（（y * k）lt x）then（x，y）::（♯genL k（♭xs））
 else genL k（♭xs）
  

它表示没有构造函数，在流中。我有一个解决方案，我会创建一对记录，然后它会起作用。除此之外，还有其他方法可以访问元素。

解决方案

构造函数是_∷_ （键入 \ :: 得到∷），而不是 $ b

b

I have made a stream of (N x N) type. How can i access the individual element of the pair ??

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

It says there is no constuctor , in stream. I have one solution in mind that i will create records of pair then it will works. Apart from that is there any other way to acccess the element.

解决方案

The constructor is _∷_ (type \:: to get ∷), not _::_.

Anyway your definition is not productive and doesn't convince the termination checker.

这篇关于在Agda中访问Stream中的元素的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！