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【关系的性质】

全部评论

相关推荐

头顶尖尖的程序员:我也是面了三四次才放平心态的。准备好自我介绍,不一定要背熟,可以记事本写下来读。全程控制语速,所有问题都先思考几秒,不要急着答,不要打断面试官说话。
点赞 评论 收藏
分享
评论
点赞
收藏
分享

创作者周榜

更多
牛客网
牛客网在线编程
牛客网题解
牛客企业服务