INDPROP.归纳定义命题.归纳关系
Inductive Relations
一个由数字（如ev）参数化的命题可以被认为是一个属性——也就是说，它定义了nat的子集，即命题可证明的那些数字。同样，一个双参数命题可以被认为是一种关系——也就是说，它定义了一组可证明命题的对。
【学习】函数语言程序设计 文章被收录于专栏
函数语言程序设计 Coq章节 Ch1 Basics【COQ中的函数编程】 Ch2 Induction【归纳法证明】 Ch3 Lists【使用结构化数据】 Ch4 Poly【多态性与高阶函数】 Ch5 Tactics【更基本的战术】 Ch6 Logic【COQ中的逻辑】 Ch7 IndProp【归纳定义命题】 Ch8 Maps【全图和局部图】 Ch9 Rel【关系的性质】
