羡慕

北京有木有极光看。。。

红色的也好

哭唧唧

不会 haskell 真的有可能学会 lean 吗？

Wu’s method uses the Euclidean algorithm with pseudo-division to solve Euclidean geometry problems. See chapter 5 of John Harrison, Handbook of Practical Logic and Automated Reasoning.

。。这个怎么感觉好像以前有人出过？。。。

（I mean 在不能应用高斯消元的情况下。。用 euclid 算法做消元。。）

Not to be confused with ㅏ, ト, or 卜.

CJK 全家桶闹麻了。。

现代语言好像即是编译语言也是解释语言= =

问一个语言是解释语言还是编译语言好像已经意义不大。。。。