Haskell

Haskell 中文群 

u-chehbefifh 1 month ago
"1100110011001100000011000000111111001100111111001111110000000000000011001111110011111100111111000000110011001111110000001111110011001100000011"
u-chehbefifh 1 month ago
几何证明可以做吗?
u-chehbefifh 1 month ago
1表示高电平,0表示低电平
u-fecd 1 month ago
"七页: 证明 a+b = b + a" - - - - - - - - - - - - - - - 这种太简单了,出新手村可以试试 a+a=b+b → a=b
u-agfgb 1 month ago
反证法是神器
u-hei 1 month ago
让大家感觉只需知道加法、乘法、结合律、分配律、交换律就掌握了一半
u-fecd 1 month ago
现在这些试图拿proof assistant往数学界推的,肯定得拿出让现在的mathematics researcher觉得interesting的东西,不然就只能是小圈子自嗨
u-ihahib 1 month ago
(不过感觉几何证明很少会用到这个
u-cbgb 1 month ago
非交换群的话当a或b为单位元时成立
u-ihahib 1 month ago
从来没能理解过PA中non-trivial的东西[Facepalm](还没
u-hei 1 month ago
"仄仄: 证明 a+b = b + a" - - - - - - - - - - - - - - - 证明 a, b <- S,S 的 + 构成阿贝尔群[旺柴]
u-fecd 1 month ago
Lean那当然是大公司…
u-fecd 1 month ago
我目测证明不了
u-agfgb 1 month ago
自然数定义第五条就是数学归纳法
u-chehbefifh 1 month ago
这个简单,用归纳法就可以
u-fecd 1 month ago
"千里冰封: 主要是,我现在又开始觉得编程和编译很重要了" - - - - - - - - - - - - - - - 就,只做数学,对这些类型系统来说我感觉太暴殄天物了[旺柴]
u-chehbefifh 1 month ago
Lean的发展现状如何
u-ihahib 1 month ago
也对噢 忘了这事 讨论的是构造性证明
u-dd 1 month ago
几年前接触的了,当时单纯对FP感兴趣,不过后来投奔了racket,现在想搞一搞type system就准备深入一下haskell
u-agfgb 1 month ago
a 和 b 是什么?自然数吗?
u-chehbefifh 1 month ago
@薛旭,你是为什么学Haskell的呢
u-cbgb 1 month ago
应该可构造一个表述但表述提及的对象不可构造[Doge]
u-hei 1 month ago
向老一辈推,就不太必要了
u-fecd 1 month ago
可能这就是返璞归真吧[旺柴]本来距离是用实数搞的
u-fecd 1 month ago
哦,但我目前见过的用戴德金分割的都是用来弄实数的…
u-bhaddf 1 month ago
technically 90后是80后的子集?
u-fecd 1 month ago
我上面说的基本群,identical的truncation is equivalence,这些都太简单了
u-agfgb 1 month ago
排中律牛批
u-facafichciiiheihbb 1 month ago
这群里90后少吧?
u-dd 1 month ago
😂快22了,刚研究生入学
u-ee 1 month ago
a和b就需要约束了
u-fecd 1 month ago
"parker_liu: https://github.com/rise-lang/shine" - - - - - - - - - - - - - - - 你是不是给我发过这个
u-fecd 1 month ago
LinearType不难搞的
u-ee 1 month ago
都是计算引起的 刚开始人们还觉得负数没有意义
u-fecd 1 month ago
"千里冰封: 步骤比直接写要长一些" - - - - - - - - - - - - - - -
u-ffeagdj 1 month ago
用LT简直。。。 不好用~
u-chehbefifh 1 month ago
不记得了,发过相关的论文给你
u-fecd 1 month ago
这种东西很适合用PA来辅助
u-fecd 1 month ago
有的毛子数学家拿ctt形式化格罗滕迪克群之类的 让我觉得有点不可理喻说实话 () 我比较看好 Agda 和 Arend,但是两边人手都没有 Lean 多
u-fecd 1 month ago
你可以假设存在
u-fecd 1 month ago
我看Idris2的synthesis简直了
u-cbgb 1 month ago
不是说平面几何用 Grobner 基基本可以代数自动证明了么
u-dd 1 month ago
Hi,我是一名学生,偶尔用haskell写写demo,请多关照
u-fecd 1 month ago
Quantitative TT可能会好许多吧
u-fecd 1 month ago
步骤比直接写要长一些
u-fecd 1 month ago
"工业聚: 让大家感觉只需知道加法、乘法、结合律、分配律、交换律就掌握了一半" - - - - - - - - - - - - - - - 那都还只是本科低年级代数呢[旺柴]
u-cbgb 1 month ago
然后平几就没有 proof assistant 什么事了
u-fecd 1 month ago
最近在想这方面的事
u-chehbefifh 1 month ago
输出是