Agda编程语言

Agda 的精髓是什么?

如何用 Agda 撰写可读的数学证明?

Colliot9/24/2018, 12:38:20 PM

请使用 Relation.Binary.PreorderReasoning,这是一个非常美妙的证明库,可以让你的Agda代码和尻可一样可读

ice10009/24/2018, 12:47:29 PM

https://github.com/ice1000/Books/tree/master/Wow-FV-zh

ice100010/9/2018, 7:08:52 PM

Preview:

Cancel

Elsewhere

goldimax replied to 一个合理的软件自动更新方案是什么?

每次启动了以后查发布 log 或是 hash 吧,现在大部分是默认这样,不过有些支持用户设定我觉得更人性化。

Hexixi replied to 在论文为什么经常使用“我们”这个词

让读者感到亲切?

Colliot replied to 虎哥这垃圾网站真的支持Kotlin的高亮吗?

这是正确的表现吗?

ice1000 replied to 虎哥这垃圾网站真的支持Kotlin的高亮吗?

是因为这个 operator 被当成了 companion object 的名字

Colliot replied to 为森么注册取名至少五个字符

骚气的是什么?

dotLyzh replied to 移动端应用设计是否并用不到「卡片」?

可以学zhihu那样用线条来分割块吖(好像现在改了

Colliot replied to 虎哥这垃圾网站真的支持Kotlin的高亮吗?

我不懂 Kotlin,你這個 倒數第三行的 operator 沒有高亮,是為什麼呢?

ice1000 replied to 设立评论功能是为了不干扰主体,是吗?

评论里用来放非回答但对问题相关的讨论。评论不能被down vote,也不能被up vote,但可以被推荐和举报。

ice1000 replied to 这个网站的存在意义已经衰变成了批判虎哥

可以不错,至少有点样子了,点名表扬虎哥