授業でBメソッドに入門してきた。 参考文献:「先端スキル開発特別講義?：形式手法を使ったデータ指向モデリングと検証」の資料 http://honiden-lab.ex.nii.ac.jp/u-tokyo/lecture2009/ BメソッドのツールであるAtelier Bのマニュアル http://www.atelierb.eu…

概要 Coqの些末な話。 proj2_sigの定義が読めなかったのでletについて調べた。 (* proj2_sig = fun (A : Type) (P : A -> Prop) (e : sig P) => let (a, b) as e0 return (P (proj1_sig e0)) := e in b : forall (A : Type) (P : A -> Prop) (e : sig P), P …