Skip to content

Instantly share code, notes, and snippets.

srbmiy srbmiy

View GitHub Profile
View tekitou.sh
#!/bin/sh
#export WORKDIR=/cygdrive/c/Users/tmiy/Desktop
#export RE="<a href=\".*\""
#export FILTERED=./testdata.txt
## main ##
cd /cygdrive/c/Users/tmiy/Desktop/Apple_files ##
grep -irho "<a href=\".*\"" ./ > ../testdata.txt ##
sed -e "s/\"//g" ../testdata.txt | sed -e "s/<A HREF=//g" > ../testdata2.txt ##
##cat ../testdata.txt ##
##cat ../testdata2.txt ##
View hoge2.v
Require Import ssreflect.
Axiom SET : Type.
Definition Var := nat.
Definition Term := nat.
(*
Definition equalS : nat := 0.
@srbmiy
srbmiy / ssrzfc002.v
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.
@srbmiy
srbmiy / ssrzfc001.v
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)).
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 *)
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.
@srbmiy
srbmiy / linux.emacs.el
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 ;;
You can’t perform that action at this time.