田春冰河
2019-10-23 00:00:00 发布
[1/3] 我给 HOL4 贡献的概率论代码是以 Concordia HVG 那帮人的工作为基础的，因为我从他们官网下载的证明代码根本无法编译，所以我一直在做的就是修复他们的代码然后提交给 HOL 官方。昨天我去拉他们的最新代码时发现他们竟然反过来也抄我的代码，还管我叫 "HOL4 github developer"。我表示开心。