Agda2では、dataで定義したデータ型は有限で、それを利用する再帰関数も停止性が証明できないといけないけれど、codataは、停止しない再帰関数を記述することができます。定義は、ラベルがcodataである以外、dataと同じです。以下のStream Aは、List Aと同じ…