環境とか色々忘れたけどmacでcabalでconduit入れようとしたら失敗した。 The Glasgow Haskell Compiler (GHC) on OS X 10.9... これ参考にやっていけた 以上 ついでにすごいHaskell学ぼう！

https://coq.inria.fr/を見ていたら、Documentationのところにこんなものがあった。 https://cel.archives-ouvertes.fr/file/index/docid/459139/filename/coq-hurry.pdf ここにSearchのことが少し書いてあって、SearchRewriteで望むものが出てこない理由が…

進捗あまりない。 update · 702639b · totem3/coq-prac · GitHub 全然わからんのでもうImportしたのを使って証明せずに進めているｗ できるところはそこまでにでてきた定理を使って証明して、まぁなんとなく感覚はわかってきたようなきていないような。 こう…

Coq入門 - 2.1 - エンジニアですよ！ に追記したが、Lemma le_n_0_eqが証明できた あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。 False_indやFalseの証明の仕方が少しわかった。 しかし、その後も証明ははかどら…

題名の通り。 効いてなかった。 よくわからんのでスルーしていたが、ストレスフルなので治すことにした。 Auto Complete Modeユーザーマニュアル auto-completeの情報は↑に素晴らしくまとまっていて、簡単に対応はわかった。 ダウンロードしたauto-complete…

進捗ありません。 疑問メモ 矛盾を示すのが難しい forall n:nat, S n <= 0 と forall n:nat, S n > 0 があれば矛盾を示すのは簡単に見える けど、どうやるのかわからない forall n: nat, S n <= 0 はPropということでいいんだよな・・ CheckしてみるとPropと…

totem3/coq-prac こういうのをやることにした。 ただCoqの標準ライブラリからLemmaとTheoremを取り出してきただけ。 こんな初歩的なものなら簡単に証明できるだろ＼(^o^)／ と思っていたら、いきなりできない・・・ｗ Lemma le_n_0_eq n : n <= 0 -> 0 = n. …

Agda入門にまんまと失敗して、Coqを入門してみることにした。 プログラミング Coq このチュートリアルをやっている。 色々調べてみると結構他にも入門はあって、先に調べるべきだったと思ったりした。 で、このチュートリアルは、とりあえず手を動かしてみる…

Amazonが届けてくれないっていうから買ってきた 人気なのか、そもそもちょっとしか入荷してないのか・・・ でもこれおもしろい！ アルゴリズムっていうと手続き型のものが多くて関数型のってそんなにない（気がするだけ）から、うれしい。 値段の割りに薄く…

そもそもはProofGeneralが使いたいがためにEmacsを使い始めたが、とりあえずAgdaをやめてCoqをいじるようになった今、vimscripts/coq_IDEというやつでもいいかもしれないと思い始めているが・・・ Macでの導入は簡単。 homebrewを使う.もう何でもこれに頼っ…

ProofGeneralが使いたいがために使い始めたが、やはりvimに慣れているのでなかなかemacsの操作は難しいところがある。 うまくいかないところを書いて解消できたら更新していく。 text objectがないのは辛い → thingoptでそれっぽい操作を http://dev.ariel-n…

Getting Started Emacs - エンジニアですよ！ でpackage.elを使ってパッケージ管理を始めた。 しかし！！ 時代は既に先に進んでいた。 Cask, Palletなるものが現れていた OMG https://github.com/cask/cask あのnaoya-itoも既に乗り換えているではないか htt…

agdaに挑戦して即死した話 - エンジニアですよ！ で書いたように、emacsが必要になった そこで、emacsを入門することにした。 vimに慣れすぎて頭がvimベースになっているが、emacsはemacs. 別のエディタなので別の考え方をしないといけなそう。 やってみてと…

agdaに挑戦し、即死した話 agdaは公式のチュートリアル(http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.Othertutorials)に日本語の記事があったので、それをやることにした http://ocvs.cfv.jp/tr-data/PS2008-014.pdf こいつだ。 その前にまずagda…

Android Studioでエミュレータを起動しようと思った時に、 emulator: ERROR: x86 emulation currently requires hardware acceleration! Please ensure Intel HAXM is properly installed and usable. CPU acceleration status: HAX is not installed on thi…

最近rubyを書くようになってrakeが便利すぎてPHPで書いてることを後悔している今日このごろだけど、相変わらずlaravel. laravelでArdentを使うと便利、が・・ - エンジニアですよ！ で、Ardentのフックを使おうと思ったんだけどArdentがダメっぽいというのを…

LaravelのValidationは便利。 http://laravel.com/docs/4.2/validation#basic-usage にある例を引用すると $validator = Validator::make( array( 'name' => 'Dayle', 'password' => 'lamepassword', 'email' => 'email@example.com' ), array( 'name' => 'r…

laravel - Model で Validation したい? それならば Ardent だ！ - Qiita こういう記事を読んだり、削除する前のvalidationをcontrollerに書きまくるのが嫌だったのでhookを削除前のvalidationもsaveの時と同じように簡単にやりたいなぁなどと思っていて、Ar…

コンパイラつくろー - エンジニアですよ！で書いたように、コンパイラを作っている。 まぁまだ難しいのでコンパイラというか単に数式をパースして計算するというのを作っている。。 アセンブリコードを出力しようとして色々試していたら、パーサー部分がまだ…

難しいのでこれとかを読みまくる以上のことはできない(；´Д｀) プログラムはどう動くのか? 〜 ELFの黒魔術をかいまみる kernelかー。触れたことがない領域。

コンパイラつくろー - エンジニアですよ！で書いたようにコンパイラを作っている。 フロントエンドもさることながらバックエンドの難しさは自分の理解できる範囲を余裕で超えている。 気になることを調べながら地道に進めていく。 ELFヘッダーについて調べつ…

最近は前に比べてちょっとレイヤーが低めな仕事をするようになり、わからないことが増えた。 中でもc言語やメモリのこと、cpuのことなどなどは全くもってわからない。 ミドルウェアはcで書かれていることが多かったり、ハード的な制約に影響されることが出て…

（laravelのコードを読んでいたけど、ドキュメントまず読めという電波を受信してせっせとドキュメントを読んでいたら、色々勉強する必要に迫られて別のことやっている。） 例えばchef。 chefとかcookbookとかrecipeとかknifeとか、無知なのでネーミングにイ…

ルーティング周りを読んでいて気になった内部的なローディングのことを少し確認しておく。 laravelはたくさんのServiceProviderが提供するサービスを利用して動いている(?) ServiceProviderをregisterすることで、色々なところから使える状態になる https://…

Modelで引っかかったところがあって先に読んだけどまず気になるのはやはりルーティング周りになるよね。 読んでみる プロジェクトを作ると、app/routes.phpが作られる 初期状態だと Route::get('/', function() { return View::make('hello'); }); となって…

プロジェクトを作った時に作られるファイルを眺めていて、モデルを見ていると class User extends Eloquent implements UserInterface, RemindableInterface ですと。 Eloquentってなんだ。 laravelが独自のORMのことをEloquent ORMって呼んでいるのはわかる…

導入 最近はやりのPHPのWeb Application Framework, Laravelを使うことにした laravel自体の勉強と、色んなコード読んで設計や実装について学ぼう月間の一環として、実装中に気になったところのコードをちょいちょい読んでくことにする。 読むのはLaravel ve…

Facebookのアプリなんて今更誰が作るのかというのはおいといて、facebook apiを野暮用で使うことになったが、このcallbackで苦労した・・。 php-sdk-4を使ってfacebook loginを使おうとしていたけど、ちゃんと実装はできていてfacebookに遷移まではするが、…

いつからかuniteのバージョン上げてからか、unite-outlineが動かなくなってた。 使おうとするとエラーが出る Error detected while processing ~/.vim/bundle/unite-outline/autoload/unite/sources/outline.vim: line 52: E121: Undefined variable: g:unit…

# というのはこういうやつ → ({type λ[α]=State[S, α]})#λ 先日のscalaz勉強会でも質問があって触れられていましたが（↓） http://t.co/GoCDB4TGVu "Scalaにおける型パラメータの部分適用 [({type F[X] = G[A,X]})# F] について" #scalaz— Kenji Yoshida (@x…