無限長のリストであるStreamは、 Idrisではlibs/prelude/Prelude/Stream.idrで以下のように定義されている。 ||| An infinite stream data Stream : Type -> Type where (::) : (value : elem) -> Inf (Stream elem) -> Stream elem これは以下と同等だそう…