#归纳类型

CIC 理论介绍：归纳构造演算

CIC（Calculus of Inductive Constructions）是现代交互式定理证明器的核心理论基础。它在 CoC 的基础上增加了归纳类型，统一地表达程序、数学命题和证明。