Haskell

Haskell 中文群

u-chehbefifh 2 years ago
"1100110011001100000011000000111111001100111111001111110000000000000011001111110011111100111111000000110011001111110000001111110011001100000011"

u-chehbefifh 2 years ago
几何证明可以做吗？

u-chehbefifh 2 years ago
1表示高电平，0表示低电平

u-fecd 2 years ago
"七页: 证明 a+b = b + a" - - - - - - - - - - - - - - - 这种太简单了，出新手村可以试试 a+a=b+b → a=b

u-agfgb 2 years ago
反证法是神器

u-hei 2 years ago
让大家感觉只需知道加法、乘法、结合律、分配律、交换律就掌握了一半

u-fecd 2 years ago
现在这些试图拿proof assistant往数学界推的，肯定得拿出让现在的mathematics researcher觉得interesting的东西，不然就只能是小圈子自嗨

u-ihahib 2 years ago
（不过感觉几何证明很少会用到这个

u-cbgb 2 years ago
非交换群的话当a或b为单位元时成立

u-ihahib 2 years ago
从来没能理解过PA中non-trivial的东西[Facepalm]（还没

u-hei 2 years ago
"仄仄: 证明 a+b = b + a" - - - - - - - - - - - - - - - 证明 a, b <- S，S 的 + 构成阿贝尔群[旺柴]

u-fecd 2 years ago
Lean那当然是大公司…

u-fecd 2 years ago
我目测证明不了

u-agfgb 2 years ago
自然数定义第五条就是数学归纳法

u-chehbefifh 2 years ago
这个简单，用归纳法就可以

u-fecd 2 years ago
"千里冰封: 主要是，我现在又开始觉得编程和编译很重要了" - - - - - - - - - - - - - - - 就，只做数学，对这些类型系统来说我感觉太暴殄天物了[旺柴]

u-chehbefifh 2 years ago
Lean的发展现状如何

u-ihahib 2 years ago
也对噢忘了这事讨论的是构造性证明

u-cbgb 2 years ago

u-dd 2 years ago
几年前接触的了，当时单纯对FP感兴趣，不过后来投奔了racket，现在想搞一搞type system就准备深入一下haskell

u-agfgb 2 years ago
a 和 b 是什么？自然数吗？

u-chehbefifh 2 years ago
@薛旭，你是为什么学Haskell的呢

u-cbgb 2 years ago
应该可构造一个表述但表述提及的对象不可构造[Doge]

u-hei 2 years ago
向老一辈推，就不太必要了

u-fecd 2 years ago
可能这就是返璞归真吧[旺柴]本来距离是用实数搞的

u-fecd 2 years ago
哦，但我目前见过的用戴德金分割的都是用来弄实数的…

u-bhaddf 2 years ago
technically 90后是80后的子集？

u-fecd 2 years ago
我上面说的基本群，identical的truncation is equivalence，这些都太简单了

u-agfgb 2 years ago
排中律牛批

u-facafichciiiheihbb 2 years ago
这群里90后少吧？

u-dd 2 years ago
😂快22了，刚研究生入学

u-ee 2 years ago
a和b就需要约束了

u-fecd 2 years ago
"parker_liu: https://github.com/rise-lang/shine" - - - - - - - - - - - - - - - 你是不是给我发过这个

u-fecd 2 years ago
LinearType不难搞的

u-ee 2 years ago
都是计算引起的刚开始人们还觉得负数没有意义

u-fecd 2 years ago
"千里冰封: 步骤比直接写要长一些" - - - - - - - - - - - - - - - ↑

u-ffeagdj 2 years ago
用LT简直。。。不好用~

u-chehbefifh 2 years ago
不记得了，发过相关的论文给你

u-fecd 2 years ago
这种东西很适合用PA来辅助

u-fecd 2 years ago
有的毛子数学家拿ctt形式化格罗滕迪克群之类的让我觉得有点不可理喻说实话 () 我比较看好 Agda 和 Arend，但是两边人手都没有 Lean 多

u-fecd 2 years ago
你可以假设存在

u-fecd 2 years ago
我看Idris2的synthesis简直了

u-cbgb 2 years ago
不是说平面几何用 Grobner 基基本可以代数自动证明了么

u-dd 2 years ago
Hi，我是一名学生，偶尔用haskell写写demo，请多关照

u-fecd 2 years ago
Quantitative TT可能会好许多吧

u-fecd 2 years ago
步骤比直接写要长一些

u-fecd 2 years ago
"工业聚: 让大家感觉只需知道加法、乘法、结合律、分配律、交换律就掌握了一半" - - - - - - - - - - - - - - - 那都还只是本科低年级代数呢[旺柴]

u-cbgb 2 years ago
然后平几就没有 proof assistant 什么事了

u-chehbefifh 2 years ago
https://github.com/rise-lang/shine

u-fecd 2 years ago
最近在想这方面的事

u-chehbefifh 2 years ago
输出是

tomato-pie
Peek into your working status with ease.