@hpcesia 没人写过,但Lean + Verso也许有这样的潜力。比如
https://lean-lang.org/theorem_proving_in_lean4/Propositions-and-Proofs/#conjunction
鼠标悬空`And.intro`就可以看到type。悬浮是个好主意但没人加这个功能。有人有空的话应该把陶轩哲用Lean写的Complex Analysis转化为像这样的一本交互式教材。
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
history = (λx. x x) (λx. x x)
When life gives you lemons, don't make lemonade. Make life take the lemons back! Get mad! I don't want your damn lemons, what the heck am I supposed to do with these?