問題タブ [codata]

Clojure で無限遅延フィボナッチ数列を与える次の関数を想像してください。

仮定

1. 私たちは、codata の簡潔な定義を「Codata は、無限の可能性がある値が存在する型である」と考えています。
2. この Clojure の例は (core.typed からの) 静的型システムを使用していないため、codata の記述はすべて「作業定義」です。

私の質問は - 上記の関数のどの部分が「codata」ですか。無名関数ですか？それは怠惰なシーケンスですか？

リスト用はあるのにストリーム用filter : (a -> Bool) -> List a -> List aがないのはなぜですか?filter : (a -> Bool) -> Stream a -> Stream a

同様の仕事をするための代替手段はありますか？

Jesper Cockx と Andreas Abel によるこの論文CoNatから引用した の定義を試しています。

私は定義zeroし、plus：

そして、私は二相似性を定義します:

しかし、私は と似ている証明に行き詰まっていplus zero nますn。私の推測では、証明には (少なくとも) with-clause for が必要ですiszero n:

しかし、Agda は次のエラー メッセージに対して不平を言っています。

この証明はどうすればできますか？