少し良くなったので、Agdaをいじってます。
⊥-elim : ∀ {w} {Whatever : Set w} → ⊥ → Whatever
⊥-elim ()
ってのがあるらしい。矛盾からはなんでも出てくるってやつね。
否定もあるんだが、
contradiction : ∀ {p w} {P : Set p} {Whatever : Set w} →
P → ¬ P → Whatever
contradiction p ¬p = ⊥-elim (¬p p)
¬が、どこで定義されてるのかわかんないんだけど。
なんか、うまく使えん。Agdaのネット上の情報のなさは笑える。空集合をなんとかしたいだけなんだが...
No comments:
Post a Comment