Kazuhiko Sakaguchi pi8027
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| 89d185fa3e0d3620703ad4b723ef85695ce427da6235fe91d74fc22d1ffcfd5d coq-8.3pl5.tar.gz | |
| f46ae5b6f0bea9dc299de6f3c020ee75c40581e32a1832e9a290d098a6a2424d coq-8.4.tar.gz | |
| 5d0e4553ab50677a94b4d5ca1650a90718e9362082a649ba95be4010390a0f80 coq-8.4pl1.tar.gz | |
| fb719a38f613b01861e3b251e745a5c8ef395a26ce7029668e85ac75fcbca2d8 coq-8.4pl2.tar.gz | |
| 97583d637f981c5554007f4e99ce6420ebc737186b1d021bd71766fd891cfb38 coq-8.4pl3.tar.gz | |
| 85a728e28346dec378d5437f7c409eab20bd42aa528b5f873cb0c9827d5baaa3 mathcomp-1.5rc1.tar.gz | |
| 5d0769c1639dcccbfe57407591ddfc12dee163c46fc012b307f17aedb5ab4d1d ssreflect-1.4-coq8.3pl4.tar.gz | |
| f044de8f75008000caf0ad61829f936384ee2d4b5fa40630352826c07b125dfb ssreflect-1.4-coq8.4.tar.gz | |
| f85d8ced769b6c38a499681a52480f2e0b9b7a0a8f028a3d35ecd1794ae64fc2 ssreflect-1.5rc1.tar.gz |
pi8027
/ gist:8272265
Last active
January 2, 2016 07:49
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| /switch { % key cases otherwise <switch> any | |
| 2 index null eq { | |
| exch pop exch pop | |
| } { | |
| 1 index 3 index known { | |
| pop exch get | |
| } { | |
| exch pop exch pop | |
| } ifelse | |
| } ifelse |
pi8027
/ gist:7929924
Last active
December 31, 2015 03:49
— forked from k16shikano/gist:7924591
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \def\lst@Init#1{% | |
| \begingroup | |
| \ifx\lst@float\relax\else | |
| \edef\@tempa{\noexpand\lst@beginfloat{lstlisting}[\lst@float]}% | |
| \expandafter\@tempa | |
| \fi | |
| \ifx\lst@multicols\@empty\else | |
| \edef\lst@next{\noexpand\multicols{\lst@multicols}} | |
| \expandafter\lst@next | |
| \fi |
pi8027
/ gist:6334409
Created
August 25, 2013 15:22
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| zero = lambda f: lambda x: x | |
| succn = lambda n: lambda f: lambda x: f(n(f)(x)) | |
| true = lambda x: lambda y: x | |
| false = lambda x: lambda y: y | |
| negb = lambda b: lambda x: lambda y: b(y)(x) | |
| iszero = lambda n: n(lambda x: false)(true) | |
| predn = lambda n: n(lambda p: lambda f: f(p(false))(succn(p(false))))(lambda f: f(zero)(zero))(true) | |
| subn = lambda n: lambda m: m(predn)(n) | |
| leq = lambda n: lambda m: negb(iszero(subn(m)(n))) | |
| modn = lambda n: lambda m: n(lambda n: leq(m)(n)(subn(n)(m))(n))(n) |
pi8027
/ icfpc2013.v
Created
August 12, 2013 12:13
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import | |
| Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool Ssreflect.eqtype | |
| Ssreflect.ssrnat Ssreflect.seq | |
| Coq.Logic.JMeq Coq.Bool.Bvector Coq.PArith.BinPosDef Coq.NArith.BinNat. | |
| Set Implicit Arguments. | |
| Axiom (PrintAxiom : forall (T : Type), T -> Prop). | |
| Theorem minn_idPr' m n : n <= m -> minn m n = n. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| * 1日目西 | |
| あ-16a「となりのチベくん」 | |
| - 接触編 |
pi8027
/ key-manager-config
Last active
December 10, 2015 16:18
SSH の鍵を発行して scp したり authorized_keys を書き換えに行ったりするツール。
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/bin/sh | |
| # ~/.ssh/key-manager-config | |
| # $1 に鍵の名前を取り、それが正しい名前であれば、1行目にその秘密鍵を持って良い計 | |
| # 算機のリストを、2行目にその鍵で入れるようにする計算機のリストを出力する。 | |
| case "$1" in | |
| master) | |
| echo | |
| echo hostA hostB www.coins.tsukuba.ac.jp |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| * 1日目西 | |
| れ-72a となりのチベくん | |
| - となりの８０１ちゃん発動編。 (1000円) | |
| * 3日目東 | |
| A-42a KEI画廊 | |
| - 画vol.11 | |
| A-80ab むてけいファイヤー/ロマンス |
pi8027
/ README.mkd
Created
October 16, 2012 20:56
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/bin/bash | |
| usage_exit(){ | |
| echo "usage: pagenum [-o offset] file.pdf" 1>&2 | |
| exit 1 | |
| } | |
| pagenum_ps(){ | |
| cat <<EOT | |
| /input (%stdin) (r) file def |