module what_happen where data Unit : Set0 where unit : Unit {- data X : Set0 -> Set0 where 要素(canonical element)が無いというコレでも -} data X : Set0 -> Set0 where x : X Unit -- xは定義したものの意味は無い nonsense : X -> Unit -- nonsens…

ranha 10月10日ぐらいに、簡単に定理証明系で殴り合うみたいなイベント無いかなぁ。メジャーな○○の使い方も、各々異なる所があるので、やってる人が個別にスタイルを教えてくれたりすると手っ取り早くて良いかなーとか。Proof Generalというかtacticalな証明…