Skip to content

Instantly share code, notes, and snippets.

srbmiy srbmiy

Block or report user

Report or block srbmiy

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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.