ちょっと基本的なところから行こう。 pCICと書いているが、まあ多くの人はそんなもの知るまい。 ちなみに、Coqについてそれなりの知識を持っていることを前提に話をするので、せめて利用者としての経験を要求する。 pCICはpredicative Calculus of Inductive…
引用をストックしました
引用するにはまずログインしてください
引用をストックできませんでした。再度お試しください
限定公開記事のため引用できません。