Inductive Definitions in the System Coq: Rules and Properties
edited by: M. Bezem, J. F. Groote
In the pure Calculus of Constructions, it is possible to represent data structures and predicates using higher-order quantification. However, this representation is not satisfactory, from the point of view of both the efficiency of the underlying programs and the power of the logical system. For these reasons, the calculus was extended with a primitive notion of inductive definitions . This paper describes the rules for inductive definitions in the system Coq. They are general enough to ...