{{ message }}

Instantly share code, notes, and snippets.

# srbmiy srbmiy

Created Mar 9, 2015
Created Jan 17, 2015
View hoge2.v
 Require Import ssreflect. Axiom SET : Type. Definition Var := nat. Definition Term := nat. (* Definition equalS : nat := 0.
Created Dec 23, 2014

View ssrzfc002.v
 (*--- Kuratowski's Definition of ordered-pairs ---*) Definition ordered_pair (x y : SET) : SET := { {{x}} , { x , y } }. Notation "\( x , y \)" := (ordered_pair x y) (at level 35). Lemma 補題_Singletonのequality : forall (x y z : SET), {{x}} = {y, z} -> x = y. Proof. move=> y x z; move. case=> Hsingleton. assert ( x ∈ {x, z} ) as Hxinx.
Created Dec 21, 2014
ZFCカッコ仮
View ssrzfc001.v
 Require Import ssreflect ssrbool. Axiom SET : Type. Axiom membership : SET -> SET -> Prop. Notation "x ∈ y" := (membership x y) (at level 100) : type_scope. Axiom Extensionality : forall (x y: SET), (forall (z : SET), ((z ∈ x) <-> (z ∈ y))) <-> (x = y). Axiom emptyset : SET. Axiom EmptySetAxiom : (forall (z: SET), ~(z ∈ emptyset)).
Created Dec 20, 2014
View ssrnat002.v
 Require Import ssreflect ssrbool ssrnat. (* Software Foundation 練習問題: ★★, recommended (basic_induction) *) Lemma ゼロを掛けるとゼロになる : forall (n:nat), n*0 = 0. Proof. move=> n. induction n as [| m]. trivial. (* 0*0 == 0 *) rewrite mulSnr. (* m.+1 * 0 ~~~> m * 0 + 0 *)
Created Dec 20, 2014
View ssrnat001.v
 Require Import ssreflect ssrbool ssrnat. Definition nand_b (b0 : bool) (b1 : bool) : bool := match b0 with | true => (~~ b1) | false => true end. Lemma nand_lemma : forall (b0 b1 : bool), (nand_b b0 b1) = (~~(b0 && b1)). Proof.
Last active Dec 14, 2015
Emacs設定晒し
View linux.emacs.el
 ;; Ubuntuでの設定です。.emacs.dの中身とかは察して下さい ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Set-up modes ;; (show-paren-mode t) (define-key global-map [f4] 'kill-frame) (define-key global-map [f5] 'make-frame) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Program modes ;;