Agdaの無限ループ

まぁ、確かに、{-# TERMINATING #-} とかで、Agda自体が止まるかどうかは判断できてないんですけどね。

割と簡単なコードなのに無限ループしてしまう。で、部分部分で出力を調べていくんですが...

　　ばっちり合ってる

で、関数を分解してみたら

　　あーら不思議ばっちり動く

ってことは、これは Agda のbugかぁ。まぁ、

　　定理証明系なので実際に eval ことは滅多にない

わけなんですけどね... この手の bug を踏むのは大得意です。