Agda で Red Black Tree

CbC on LLVM は片付いたので(多少問題はあるが)、今度は Agda の方かなと思って。

一日かけたけど、あんまり進んでないです。つまり、二進木よりめんどいってことね。

もっと、ずっと簡単な方法もあるのかも。でも、

　　エンジンはかかってきたかな

プロシンは、これじゃなくて、Automaton の方を出すつもりです。

　　非有限 Automaton

みたいな話。