計算型goto文

なんか、あったよな〜 x と y を比較して、それによって飛び先が変わるみたいなやつ。

Agda では、

　　Trichotomous

とか格好良く呼ぶらしいです。「とら〜いこともす」

例の Decidable の三分岐版らしい。これで比較の証明の場合分けを乗り切れるかな〜

ついでに、Nat の比較 > は、Agda は三種類あるってのを発見しました。あるのは良いんだけど、相互変換ぐらい付けてくれてもいいんじゃないか?