No Such Blog or Diary

リスト l の n 番目の要素を取ってくる関数 nth n l を定義するのに (n < length l) をつけときゃデフォルト値とか使わずトータルな関数定義できるよね，とかいう勢いで関数本体を書いてみようと思ったのだけどどう書いていいのかわからなかったという．結局，定義の頭に Program ってつけといてよくわからんところに _ （アンダースコア）置いといて，あとで proof obligation を始末する，という方法で定義できることを教えたもらったのでそれで済ませたのだけど……　定義された関数が読めん．そして定義された関数に関する性質の証明も訳わからん項が出てきて混乱する（再帰先で n < length l が保たれることを示すためにこの型を持つ読めない項が作られるので式の見た目がごちゃごちゃ）．依存型とか使いこなせない気がする．

丸一日寝てた．お陰で体調もあと一晩寝れば通常運転くらいに回復．とりあえず予想以上に寝不足と冷えすぎが堪えたっぽい．今日は気温も高くて幸い．

さて，防寒対策を練っておくか．

なんの予定もない週末とか結構久しぶりな気がするなぁ……　とか言いつつ論文の印刷に大学まで出て来たり．つか，でかいディスプレイを使うには必然的に大学に出てこないとならん．

それはよいとして，頭がいたいレベルで風邪引いてるので冬眠しよう．

予想よりも寒いのでやばそうだなと思っていたら喉と鼻がやられた．とりあえず週末は寝て過ごすか．

閑話休題．

Don't disturb 無視して突っ込んで来ないで欲しいんだけど……　ちょいと移動すっか．

普通に関数型言語として使うのは問題ないけれど依存型で変なことしようかなと思い始めるあたりでごちゃごちゃと……　Prop と bool の違いではまりまくるとか．どこに気をつけるべきなのかがはっきり見えないので修行あるのみ？

Coq 8.4 用のはバグってる？　生成される関数の本体であるラムダ式が型引数を通常の引数と同様に受け取ろうとしているような気が……　関数の型が合わないという文句を言われる．どうやら Haskell を吐いても Ocaml を吐いてもおかしいらしい．

とりあえず 8.3p12 用で我慢するか……　別の部分が 8.4 の機能を使っている気がしなくもないのだけど大丈夫かな？

つか，１日に２回も coq をコンパイルすることになるとは．