なんとなく面白そうだけど、身近で使ってる人もいないし、何が便利なのかよくわからないコマンドだったgnu screen Webで断片的な情報を齧るだけだと、 Detachが便利？ 何それ？sshが切れても大丈夫？ 画面の分割が楽しい？ という二つの楽しみかたがあるよう…

パースの法則からcoqで排中律を導く。 Theorem Peirce : forall A B : Prop, ((A -> B) -> A) -> A. Admitted. Theorem classic : forall p : Prop, ~~p -> p. Proof. unfold not. intros. apply (Peirce p False). intro. exfalso. apply H. apply H0. Qed.…