コードスプリント

9時に職場に集合。スウェーデンからのAgda開発チーム3人（タフで頭の回転が速い）を加え、合計10人程度で一週間ひたすらAgda2のコードを書き続ける。会議室にこもって一日中コーディングなんて、スーパーハカーにでもなった気分。
意見交換や成果紹介も重要で、私もスウェーデンの人から、Agdaにおける変数の取り扱いについて、explicitなsubstitutionの定義の例を紹介してもらう。会話はついていくのが大変。