@hpcesia 没人写过,但Lean + Verso也许有这样的潜力。比如
lean-lang.org/theorem_proving_
鼠标悬空`And.intro`就可以看到type。悬浮是个好主意但没人加这个功能。有人有空的话应该把陶轩哲用Lean写的Complex Analysis转化为像这样的一本交互式教材。

Gavin Zhao boosted

Google announced that as of September 2026, it will no longer be possible to develop apps for the Android platform without first registering centrally with Google. This registration will involve:

- Paying a fee to Google
- Agreeing to Google’s Terms and Conditions
- Providing government identification
- Uploading evidence of the developer’s private signing key
- Listing all current and future application identifiers

keepandroidopen.org/

#android #opensource #keepandroidopen

Show older
小森林

每个人都有属于自己的一片森林,也许我们从来不曾走过,但它一直在那里,总会在那里。迷失的人迷失了,相逢的人会再相逢。愿这里,成为属于你的小森林。