2009-10-19から1日間の記事一覧

今日のCoq: ラムダ式とsubstitute

Coq

バリアントでラムダ式を作って、その上でsubstituteを定義してみました。目指してるのは単純型付きラムダ計算です。 覚えたこと 全部、末尾に「〜らしいよ」ってつけて読んでくれるとうれしいです。 再帰のあるバリアントはInductiveで定義する 相互再帰のあ…

watchコマンドを作ってみた

30分プログラム、その680。watchコマンドを作ってみました。watchコマンドって知っていますか? $ watch hogehogeとやると、一定時間ごとにhogehogeを実行して画面を更新してくれるコマンドです。 watch dateで時計変わりにしたり、watch lsでファイルが作ら…