Warning: Undefined global variable $debug in /var/www/ourcoders/tiny4cocoa/application/controllers/baseController.php on line 124
田春冰河 2020-01-10 19:08:52 发布的技术动态 - OurCoders (我们程序员)
OurCoders
  • 首页
  • 话题
  • 搜索
  • /var/www/ourcoders/tiny4cocoa/templates_c/32ccb5ef476b6269d182d4601ed2ed1ef16375bd_0.file.index.html.php on line 116

    Warning: Attempt to read property "value" on null in /var/www/ourcoders/tiny4cocoa/templates_c/32ccb5ef476b6269d182d4601ed2ed1ef16375bd_0.file.index.html.php on line 116
    ">
田春冰河
2020-01-10 19:08:52 发布
[1/3] 话说前天我提交给 HOL 官方的 400 多行代码——就是我跟大小老板合写的论文里某定理的形式化版本——已经顺利被合并了。这样我在 HOL 贡献者排名里按照新增代码行数还差不到一千行就可以晋级了。结果没想到给 HOL 提交 PR 比正式发表论文还管用，排名第二的 Konrad Slind，一个比我早学定理证明 ...全文
原文链接