2010-07-01から1ヶ月間の記事一覧

Perl6 Crash

http://atnd.org/events/6687"一応"リリースされたようなので、開催は決定です。場所を素早く押さえたい・・・。あと全然人増えないのは場所とか決めて無いぼくが悪いんですが、お願いします。

Perl6 Crash

http://atnd.org/events/6687日程が8/7(土曜日)に決まりました。あとは、ネットにつながる会場を確保しないといけないのです。 今8人にしているのは、人が多いと小回り効かなく成って場所借りられなく成ると困るかなーっていう事だからで、 ちゃんとした所が…

Perl6 Crash

http://atnd.org/events/6687を作ってみました。画像はそのまま、スタープラチナが良かった気もしますが。これは何なのかとゆーと、以前Go言語が出た時に、http://atnd.org/events/2115 というものをやったのですが、それのRakudo Star版です。 一日Perl6の…

Falsoを使ってみた?

あらまし http://twitter.com/MoCo7/status/19336249733MoCo7さんのretweetで発見ティンと来た!!!http://estatis.coders.fm/falso/なんかCoqっぽいコードがあるけど何やってるか分かりません。 Agda2で {-# OPTIONS --universe-polymorphism #-} module F…

これは停止するらしい

module IndHatena where open import Data.Nat import Level open import Induction.Nat using (<-rec) f : (x : &#8469;) -> &#8469; f zero = zero f x = f x' where postulate x' : &#8469; postulate pr : x' < x f改' : (x : &#8469;) -> ((y : &#8469;…

どっちがいいんだろう?

何かを定義する時に、 ∃n > 0.n + n > 0のように、0より大きなある自然数nを加算した結果は0よりも大きいという意味が無い命題を書きたい時に ∃n > 0といった、ある種自然数のsubtypeを作って定義を進めたい、というような時、Agda2ではどう書くのが良いんだ…

雪歩プロデュースメモ

後の為に7月13日3:20頃開始http://lambda-the-ultimate.org/node/4006 これ面白そうだなぁ。 Fランク 多分雪歩さんは晩成型なので、しょっぱなからオーディション受けまくろう!!(まぁSランク取る時はいつもその方法なんですが...あとすごいテンション下がる…

C++のぼくがよくわかってなかった話

まずこういうコードを書きます #include <iostream> using namespace std; struct S { int i; }; int main() { S s(); cout << s.i << endl; return 0; } これを最初に書いた時の気持ちは、何故か、Sのデフォルトコンストラクタを呼び出してsを〜という感じだったので</iostream>…

こわいはなし

{-# LANGUAGE TypeFamilies , ScopedTypeVariables #-} type family TF a f :: TF a -> Int f (v :: TF a) = 0 ghciに投げ込むと /Users/ranha/Haskell/proghost% ghci kowai.hs GHCi, version 6.12.3: http://www.haskell.org/ghc/ :? for help Loading pac…