pCICの細かな部分

先週の発表で、「Coqをいじりたい人向けに情報をまとめておいたら役に立ちそう」という言葉をもらった。
そんなのどんだけいるんだろう・・・と思わなくもないが、実際端から端まで読んだわけでもないし（読まなくてもブラックボックスのまま使える部分も多い）、まとめられる限りまとめるのも重要か。
そんなことを考えたが、そもそも私がみるCoqの実装部分は、pCICの細かな部分がかかわってくる話なのだ。
どないせいと・・・


というわけで、実装について少し説明する前に、pCICの話をしないとなあ、と思った次第。
論文にも書いた内容なので、そんなにここに乗せるのも難しくないはず。
分量を考えなければな。
まあ、今日これから、というわけでもないが・・・