クリスマスツリー

この手のものには特に思い入れはないですが。なんか電池で点灯するものらしいです。

昨日は Context Free Grammer を Agda で書くのにはまってました。いろいろやってみたが、

　　Non terminal にGrammer を Node の二重のリストで登録すると良いらしい

という割と「え〜、そんなの?」という感じが良いらしい。Agda は List を使うと負けっぽい感じがするんですが、

　　Grammer は有限の順序のある規則の集合
　　規則はノードの列

ということなので、素直に順序のあるListで構成するのが良いわけですね。