kabisukeのブックマーク / 2009年12月30日

kabisuke id:kabisuke

2009年12月30日のブックマーク (4件)

Coq Tips
以下、Parameters A B C P Q R : Prop. を仮定。目次前件 (仮定) が……の場合仮定が False の場合・仮定に矛盾がある場合仮定が否定の場合 (~A の形) 仮定が含意の場合 (A -> B の形) 仮定が連言の場合 (A /\ B の形) 仮定が選言の場合 (A \/ B の形) 仮定が全称量化子 (forall) の場合仮定が存在量化子 (exists) の場合後件 (ゴール) が……の場合ゴールが True の場合ゴールが False・否定の場合ゴールが含意の場合 (A -> B の形) ゴールが連言の場合 (A /\ B の形) ゴールが選言の場合 (A \/ B の形) ゴールが全称量化子 (forall) の場合ゴールが存在量化子 (exists) の場合ゴールが恒真命題 (トートロジー)
kabisuke 2009/12/30
Coq
リンク
WikiHub :: coq :: tactics.txt
仮定が... f x simpl in Hで仮定Hの簡約ができる x = y rewriteで、式の一部分を書き換える。 rewrite H with (x := 1) (y := 2)のように変数の対応を指定することもできる AssociativityOfAppend < Show. 1 subgoal A : Type a : A x : list A y : list A z : list A IHx : (x +++ y) +++ z = x +++ (y +++ z) ============================ a :: (x +++ y) +++ z = a :: x +++ (y +++ z) AssociativityOfAppend < rewrite IHx. 1 subgoal A : Type a : A x : list A y : list A z
kabisuke 2009/12/30
リンク
ターミナル用プレゼンツールをリリースいたしました - Hello, world! - s21g
LLfutureで使用した端末用プレゼンツールをリリースいたしました。 present-0.1.1 - Rubyforge present GitHub 利用法は、 READMEファイルと sample/ディレクトリの中身をご覧ください。 1 2 3 4 5 _ _ 6 |_) |_ _ ._ |_) _.o| _ 7 | \|_||_)\/ (_)| | | \(_|||_> 8 / 9 10 The Web Application Framework 11 12 s21g LLC 瀧内元気 13 14 15 1/15|** |00:02
kabisuke 2009/12/30
プレゼン

Ruby

framework

terminal
リンク
オンラインプレゼンツール「Prezi」を使ってみたけど、これはすごいかも知れない
■ オンラインプレゼンツール「Prezi」を使ってみたけど、これはすごいかも知れない少し前に話題になっていたけど使うチャンスがなかったオンラインプレゼンツール「Prezi」、社内でLTをする機会があったので使ってみた。いやぁ、これは相当面白いね。サイトにあるデモを見ればどういう感じかわかると思うけど、ぱっと見ただけではトランジションが風変わりな普通のプレゼンソフトに見える。でもこれ、既存のプレゼンツールからすると、パラダイムがまるで違う。Preziの評価で「スタイリッシュなプレゼンが簡単に作れる」みたいな言い方が多いけど、ぜんぜん違うよコレは。このアイデアは単にカッコイイとかそういうレベルじゃない。よく会社の会議なんかで、A3 1枚にExcelシート上に描かれた図表をばばーんと印刷して、それを説明するなんて場面があるけど*1、「右上のこれが××なんですが、左下にある……そう、それは○
kabisuke 2009/12/30
プレゼン

あとで読む
リンク
- 2010年1月5日
- 2009年12月30日
- 2009年12月22日