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