マンガ

休日で、何もしない一日であった。

知り合いが入院してたときに貸してたマンガが返ってきてしまったので、読み耽ってしまう。返さんでいいのに。

本日のCoq

型とか暗黙の引数とかイミフ。

型ありの言語で、pairとlistは違うもんなんだなあ。ということを知る。

Inductive prod (X Y: Type) : Type :=
 pair : X -> Y -> prod X Y.
 。。。
Fixpoint split {X Y : Type} (l : list (X*Y)) : (list X) * (list Y) :=
 match l with
 | [] => ([], [])
 | (x, y) :: l' => ((x :: (fst (split l'))), (y :: (snd (split l'))))

Example test_split:
  split [(1,false),(2,false)] = ([1,2],[false,false]).
Proof. simpl. reflexivity. Qed.
Eval simpl in split []. (* エラー！ *)
end.

splitで、nil渡すとエラーになるやん。と思いましたが、
そんなときは、nilに型を渡すか、splitに型を渡すかすりゃいいんですね。

Eval simpl in (split (@nil (nat*bool))).  (* OK *)
Eval simpl in @split nat bool [].  (* OK *)

Coqにおいて、暗黙の引数は、shのaliasみたいなもんで、
＠は、shの\みたいなもんみたいですね。