跑题了，假设你得出 forall x xs. x::xs == (rev xs) ++[x] 呃不是 x::(rev xs) == xs++[x]

（好吧二者是不一样的，记得主语始终在 ++[x] 的部分）
（注意要解构等式两边，都必须用到递归栈，第一个实际上是正向 rev 的定义😞）
可以通过以下方法证明 rev (rev xs) == xs ：

-- x::(rev xs) == xs ++[x]
xEqTail : (a, [a]) -> [a] -> Bool

idp = (==) -- eq path
revId (x::xs) = -- xs++[x]
xEqTail (x, ) && (revId xs)
revId [] = (idp [] [])

等等， x:(rev xs) == xs++[x] 这个等式不对，我没注意到 (rev xs) 和 xs 本身的区别…… 其实是 x:(rev xs) == (rev xs)++[x] ，意味着 x:xs == rxs++[x] ……
算了写不出来😢不多说了，入门科普而已。
顺便：代码部分可以理解为交换 ::(has type) 和 :(cons) 语义的 Haskell, 反正我不是说正经的。

上面证明 rev (rev xs) = xs 里我解构施用层 (rev xs) 到 x:(rev xs) = xs++[x] ，其实是 rev (x:xs) = (rev xs) ++[x] 的反向变形。

我显然把右边的 xs 理解成其参数了（虽然对正常程序猿 等式左边才能有未知量是直觉😂），没注意到关系解构的部分必须以 (rev xs) 描述，例 rev $ [1,2,3] 可不等于它++[1] 呢…… 但是 [2,3] ++[1] 就对了

这个点子是我在提示下独立想出来的，但思想和实践总是隔着基础模型的桥梁，虽然能设计、找到特色点也远不等于能细分并逐步实现，知道理论不等于善于实行。
不过，我仍希望这对大家有帮助，哪怕是理解别人的误区和失败。

只要可能对人有帮助，我才不怕出丑丢脸；毕竟相比技术和创造，自尊太微不足道了。

把 rev (rev xs) = xs 里的 (rev xs) 与 xs 互换即可得到 rev xs = rev xs 全等，可这不是“移项变号”或“两边同时减”那么简单（虽然也可理解为“把rev移到另一侧”呢），但不管怎么样显然是重组 a:rev$v=rev$a:v 这种关于 rev 结果的关系

以我目前这层面的水平当然仍是无法做到定理证明啦，虽然它也有意思。 #cs #plt

话说部分读者你们也被不明觉厉加入那个讨论组唉，还是劝退好了

人家千里冰封说的明明白白，必须有 dependent type 基础，并且他是不负责给你打基础的，狠心点：

菜鸟别以为和大牛在一起、或者看大佬做事就能给自己涨知识，没用的。

接近那个领域，也别以为自己看它的文档、用它的术语你就属于它。
系统的知识网络和直觉不是靠生硬的文字和无聊的名词能表达的，名词和定义规则背后隐含的是前人真切的思考，你不学他所学怎么能真懂他。

有些人就是天才，你和他差的就是人家能独立得出而你无法get到的一句话、一个小思路，有时候是因为知识和经验，有时候 1% 的灵感就是靠努力无法填补的。

不要以为自己足够热血或者“非常想”就能成功，科学说了算。

也不要自作主张认为“我需要那些东西来帮助进步”，不你不需要😡。阻塞在一个目标上不懂变通、提升知识广度，那叫环形等待、死锁。

说错了话他们不耐烦你也不开心，本就不是一路人，派系不同何必凑数。

#China #web 🤔

【品葱】
看到这个，我只想说：意料之中。

整天内斗吵架，不维护社区氛围、不鼓励创作，那么就只能慢慢的死亡了。因为品葱本身的竞争力不大，很容易就能找到替代品。真正让用户持续在品葱发表内容，都是靠用户维护出来的氛围。肆意将用户污蔑成网军，对原创内容的不重视，极大的破坏了这一氛围。品葱自然就丧失自己的独特性了。

更不用说趾高气昂的管理员。这点相信如果大家有和某些管理员接触过就知道我在说什么。

不重视内容，不重视用户体验的恶果已然显现出来。品葱站长无论是公开还是私下都多次表示品葱的目标是要“活下去”，而不是“做大”。但是品葱目前面临的问题是自身在失去“生命力”。错将维护讨论氛围、改善用户体验视为“扩张”。对于提出问题的用户刻薄与打压（甚至污蔑对方为网军），对于不满管理员决策的用户嘲弄与侮辱。品葱与半年前提出的《习惯法》沦为废纸。所谓“用户自治”彻底失败。可以说，品葱作为公共讨论空间，已完全失去“讨论”。目前品葱的定位更多的是内容农场而不是“问答式社区”

品葱的例子令人惋惜。曾经的旧品葱无论是氛围还是内容都无法挑剔，可惜在中共的威逼利诱下被迫关闭；新品葱在最初的时候虽然小众，但是质量、氛围、人气随着反送中运动的爆发而爆发，往后无论是反送中，新冠肺炎，都有着非常大量且用心的内容发表。可如今再去看品葱，关于国安法的讨论寥寥数个，首页大半部分被搬运新闻和旧贴占据。质量也不尽人意。看了看品葱曾经的archive，看到曾经品葱上的人们乐观而且满怀希望得为自己心中的信念与他人据理力争，再看看如今少有答案/评论超过一百个字。曾经置顶各种活动贴，多方联动。如今躲在角落里自己一个人玩泥巴

不禁感叹一句“时过境迁啊。

品葱已死，我们还要继续走下去。希望大家永远都要记得品葱，记得它曾经大放异彩，更要记得它是怎么落寞的。

各位晚安。

#gui #android

请教一个相机相关的问题。打开相机以及设置预览回调都在同一个子线程内。但是在onPreviewFrame回调方法中打印当前线程却是 main。 何故？

Callbacks from other methods are delivered to the event loop of the thread which called open(). If this thread has no event loop, then callbacks are delivered to the main application event loop. If there is no main application event loop, callbacks are not delivered.

#Kotlin #collection 怎么把两个List合为Map?

可以 (xs.zip(ys) as Iter<Pair<A,B>>).toMap() 但不一定真是 Iter
可以用 xs.associate { it to yz.next() }
可以 ys.associateBy { xz.next() }
据说还有 xs.associateWith(ys) { (x,y) -> x to y }

如果连 Pair 都不想创建，可以 zipToMap 组合+归纳:
while (xz.hasNext() && yz.hasNext())
map[xz.next()] = yz.next()

api依赖就是compile的

implementation 是 runtime，那么 runtimeOnly 又是？

天哪。 #android #java
反正我只爱 DOM 和 Model/View

现在大家用aac架构的多吗？怎么看这个架构

Android architecture components

这个跟mvvm mvp mvc相比，是不是复杂了

但是啊，我的配置已经是4G了：

@AntiRevoke
請幫忙檢舉謝謝（
Report > Other
範文：
This channel provides a "plugin" for tdesktop that breaks the delete message feature for other chat members, this plugin violates clause 1.4 of telegram's api tos, please ban this channel.