{"id":85047,"date":"2020-03-25T03:55:57","date_gmt":"2020-03-24T19:55:57","guid":{"rendered":"http:\/\/4563.org\/?p=85047"},"modified":"2020-03-25T03:55:57","modified_gmt":"2020-03-24T19:55:57","slug":"agda-%e5%9c%a8%e5%89%8d%e7%ab%af%e5%bc%80%e5%8f%91%e9%a2%86%e5%9f%9f%e4%b8%ad%e7%9a%84%e5%ae%9e%e8%b7%b5","status":"publish","type":"post","link":"http:\/\/4563.org\/?p=85047","title":{"rendered":"Agda \u5728\u524d\u7aef\u5f00\u53d1\u9886\u57df\u4e2d\u7684\u5b9e\u8df5"},"content":{"rendered":"<div>\n<div>\n<div>\n<h1>                  Agda \u5728\u524d\u7aef\u5f00\u53d1\u9886\u57df\u4e2d\u7684\u5b9e\u8df5               <\/h1>\n<p> <\/p>\n<div>\n<div> <span>\u8cc7\u6df1\u5927\u4f6c : YadongZhang <\/span>  <span><i><\/i> 10<\/span> <\/div>\n<div> <\/div>\n<\/p><\/div>\n<\/p><\/div>\n<\/p><\/div>\n<div isfirst=\"1\"> <\/p>\n<p><strong>\u5f88\u591a<\/strong>\u5927\u4f6c\u90fd\u5bf9 Agda \u548c\u524d\u7aef\u540c\u65f6\u6709\u4ea4\u96c6\uff0c\u6628\u5929\u6b63\u597d\u53c8\u53d1\u73b0\u4e86\u8fd9\u6837\u4e00\u4e2a\u9875\u9762\uff1a<\/p>\n<p><img decoding=\"async\" src=\"http:\/\/4563.org\/wp-content\/uploads\/2020\/05\/20200516_5ebfb5e841983.png\" alt=\"Agda \u5728\u524d\u7aef\u5f00\u53d1\u9886\u57df\u4e2d\u7684\u5b9e\u8df5\" \/><\/p>\n<p>\u7136\u540e\u5728\u7c7b\u578b\u63a8\u65ad\u4e0a\uff0c\u76ee\u524d\u6b63\u5728\u505a\u7684\u6bd4\u8f83\u706b\u7684\u5c31\u662f TypeScript TNG<\/p>\n<p>\u6211\u60f3\u95ee\u7684 Agda \u5728\u6b63\u5e38\u524d\u7aef\u4e1a\u52a1\u5f00\u53d1\u4e0a\u80fd\u63d0\u4f9b\u591a\u5927\u5e2e\u52a9\uff0c\u6bd4\u5982\u8bf4 <code>edge\/corner case<\/code> \u63a8\u65ad\uff0c\u7eaf\u5c5e\u597d\u5947<\/p>\n<\/p><\/div>\n<div> <b>\u5927\u4f6c\u6709\u8a71\u8aaa<\/b> (<span>1<\/span>)        <\/div>\n<div> <\/div>\n<\/p><\/div>\n<\/p><\/div>\n<ul>\n<li data-pid=\"1393796\" data-uid=\"2\">\n<div>\n<div>\n<div> <span>\u4e3b<\/span> <span>\u8cc7\u6df1\u5927\u4f6c : YadongZhang <\/span>  <\/div>\n<div> <i title=\"\u5f15\u7528\"><\/i>  <span>          <\/span> <\/div>\n<\/p><\/div>\n<div>                                                             \u627e\u5230\u7b54\u6848\u4e86\uff0c\u679c\u7136\u6bd4\u5355\u5143\u6d4b\u8bd5\u66f4\u4e25\u683c<\/p>\n<p>https:\/\/www.zhihu.com\/answer\/164882054<\/p>\n<p>\u8fd9\u6837\u662f\u4e0d\u662f\u5c31\u4e0d\u7528\u6101\u627e \u6d4b\u8bd5 \u6570\u636e \u4e86                                                            <\/p><\/div>\n<\/p><\/div>\n<\/li>\n<li>\n","protected":false},"excerpt":{"rendered":"<p>Agda \u5728\u524d\u7aef\u5f00\u53d1\u9886\u57df\u4e2d\u7684\u5b9e\u8df5 &hellip;<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":[],"categories":[],"tags":[],"_links":{"self":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts\/85047"}],"collection":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=85047"}],"version-history":[{"count":0,"href":"http:\/\/4563.org\/index.php?rest_route=\/wp\/v2\/posts\/85047\/revisions"}],"wp:attachment":[{"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=85047"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=85047"},{"taxonomy":"post_tag","embeddable":true,"href":"http:\/\/4563.org\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=85047"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}