サクサク読めて、アプリ限定の機能も多数！
トップへ戻る
iPhone 17
d.hatena.ne.jp/pi8027
完全なまとめがみつからなかったので、まとめておく。ControlMaster を使います。 REMHOST=localhost ssh -S ~/.ssh/master-$$ $REMHOST -M -f -N 2>/dev/null 1>&2 ssh -S ~/.ssh/master-$$ $REMHOST hostname ssh -S ~/.ssh/master-$$ $REMHOST uname ssh -S ~/.ssh/master-$$ $REMHOST who ssh -S ~/.ssh/master-$$ $REMHOST -O exit 1>/dev/null 2>/dev/null こんな感じで書けます。最初のsshコマンドで接続を作って、最後ので破棄しています。 scpの呼び出しも、 scp -o ControlPath=~/.ssh/master-$$ file
概要 「この設定のお陰で tmux のペインを有効活用できるようになりました！」(19歳 男性) nw(){ local CMDNAME split_opts spawn_command CMDNAME=`basename $0` while getopts dhvPp:l:t:b: OPT do case $OPT in "d" | "h" | "v" | "P" ) split_opts="$split_opts -$OPT";; "p" | "l" | "t" ) split_opts="$split_opts -$OPT $OPTARG";; * ) echo "Usage: $CMDNAME [-dhvP]" \ "[-p percentage|-l size] [-t target-pane] [command]" 1>&2 return 1;; esac done shift
この記事はTheorem Proving Advent Calendar 2011の14日目の記事です。 agda2-mode とは? Agda2 は Emacs のメジャーモード agda2-mode を持ちます。agda2-mode は Agda2 を書くのに必要不可欠な多数の機能を提供しており、これが無ければ Agda2 で証明やプログラムを記述するのがとても困難になります。 agda2-mode は、以下のような機能を提供します。 ソースコードの検査 正確なシンタックスハイライト placeholder 限定的な自動証明 コンテキストと型の表示 正規形の計算 Agda2 用の入力メソッド パターンマッチ分岐の自動生成 当然これらは Emacs Lisp で記述されていますが、その本質的な部分は Haskell で記述された Agda2 処理系を呼び出すことによって実現しています。
この記事はTheorem Proving Advent Calendar 2011の1日目の記事です。 今日は Agda2 というプログラミング言語を用いて、依存型を用いることで絶対的な安全性と Haskell や OCaml などでは(通常の方法では)実現できない柔軟さのどちらも持つプログラムを記述できるということについて書きます。 この記事は主に、普段動的型付けのプログラミング言語を使っていて、静的型付きの言語では自分の意図したものを十分に表現できないと考えている人を対象読者としています。 依存型とは 型に依存する型や、値に依存する型を作れる型のことです。 例えば、値に依存する型を用いることで型レベルでサイズが与えられているリストを作ることが可能です。 また、リストの結合関数は長さ a のリストと長さ b のリストを取り、リスト a+b のリストを返すというような型を持つことになります
してみた。 動機 スタックの操作を roll とか pop とか dup とか exch とか書いて頑張るのが煩わしかった。メタプログラミングによる解決が求められる。 Haskell による実装 最初はプリプロセッサを書くつもりでいたので。 module Stack where import Control.Applicative data Operation = OpPop | OpRoll Int Int | OpIndex Int deriving Show stackConv :: [Int] -> [Int] -> Maybe [Operation] stackConv from [] = Just $ map (const OpPop) from stackConv (f : fs) (t : ts) | f == t && (f `elem` fs || f `notElem
この記事は Haskell Advent Calendar jp 2010 のために書かれた物です。(20日目) 型推論は簡単 ML や Haskell のような言語の型推論は、型推論を知らないみなさんが考えているよりは遥かに簡単な物です。大雑把に言ってしまえば、構文木全体を探索して、同一である事が明らかな型同士の単一化をしていけば型推論できてしまうのです。 型推論の難しい所その1 - 多相型 しかし、型推論にも難しい事が無いわけではありません。まず最初の難関としては多相型が挙げられます。 ML や Haskell では let などの変数束縛に対して多相型が導入されています。式の中でこれらの変数が出現すると、その型の型変数(確定していない部分)を全て付け替える操作が発生します。 しかし、確定していない部分を付け替えるという事は、最終的に元の型が確定した後にその操作をしなければ、型を正しく
Theorem Prover Advent Calendar 2013 の21日目の記事です。 先月、信州大学で TPP 2013 という定理証明器ユーザの集会がありました。TPP では毎回証明の問題が事前に出題され、参加者の一部がこれを解いてきて発表するようになっています。これが TPPmark です。この記事は、TPPmark 2013 の SSReflect による解答例とその解説です。問題はhttp://shirodanuki.cs.shinshu-u.ac.jp/TPP/TPPmark2013_Jap.pdfを参照してください。 これ以降の証明では以下のモジュールを使います。 Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq fintype path fingraph finset fingroup perm. 1
#Stricter.org オフを終えて帰ろうかというタイミングで YAPC::Asia 2009 Hackathon に誘われたので参加してみました。場所は小飼弾さん宅でした。 YAPC とか参加していないし良く知らないし Perl とか書けないのですが、まあそういう事を気にしてはいけないと思う。 Hackathon だからといって特に作業が進んだというわけでもないのだけど、弾さん以外にも竹迫さん,Yappoさん,malaさん,奥一穂さんなど、有名な方が多くて Hackathon 的ではない意味でとても楽しかった。 あとは、竹迫さんと色々話せたのは結構大きいような気がする。記号プログラミング polyglot のスライドを見せてもらったのだけど、良い意味で間違った労力の使い方をしていて素晴らしいと思う。
anarchy golf - Gray code yuko さんが優勝でした。おめでとうございます。現時点での最良解は以下のような物。 y,u;main(k,o){for(o=~o%9;y<1<<o;y=k&-k)printf(--k?"\n%0*o":"Gray code n=%d",o,u^=y*y*y);} 因みに私の解答は、 i;main(l,j){for(printf("Gray code n=%d\n",j=l=j%5+7);!(i>>l);putchar(!j?j=l,i++,10:48|1&(i^i>>1)>>--j));} となっている。最良解が綺麗過ぎて泣いた。あと今更なんだけど、i>>1ってi/2で良いよね。!(i>>l)も1byte縮まるのではないか。 現時点での最良解を読んでみる。 o=~o%9 は定石のようなもの。入力を読まずに数打てば当たる戦法。ちゃんとやるの
このページを最初にブックマークしてみませんか？
『d.hatena.ne.jp』の新着エントリーを見る
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
