最近在用Coq的一点碎碎念… Dependent type是个很有意思的类型理论,使用值来构建类型,不过和我想象的还有点不一样…

比如使用强规范函数,需要传入值,以及对于规范的证明项.按照我的想法呢,关于值的某项证明应该是依附在值上的一个属性…而将值包裹在证明里,感觉就会怪怪的.