無限長のリストであるStreamは、
Idrisではlibs/prelude/Prelude/Stream.idrで以下のように定義されている。
||| An infinite stream data Stream : Type -> Type where (::) : (value : elem) -> Inf (Stream elem) -> Stream elem
これは以下と同等だそうだ。
codata Stream : Type -> Type where (::) : (value : elem) -> Stream elem -> Stream elem
codataである。余帰納である。
ところで以下のコードを見て欲しい。
無条件に（xs -> Q xsの間の条件無しに）Q xsが言えている。
すごくね？
これが余帰納の力か……
（何に使えるのか分からないけど）
.
.
.
