Tesla Zhang‮

主要是有很多很垃圾的人也在倡导这些，比如C#前几天那个闹得特别大的大新闻

首先我觉得应该和那个p开头的中文版C#的那个人划清界限

哦不是q开头

我修改了下 Kotlin 的和 Haskell 的，现在稍微能看了，以前那个 Hello World 式的实例感觉十分挫 23333

我已经证明了 Kotlin 中可以完美汉化 `@Test`

I really hope we can have this

This will be useful for testing, but it should be very very very ugly to expose this to the user imo

> I agree completely: filling "dumb" squares cubes that follow from the codomain having a specific h-level is entirely mechanical work that should be handled by the proof assistant. I'm...

> Hi @ice1000, > > * with [markdown](https://docs.github.com/github/writing-on-github/getting-started-with-writing-and-formatting-on-github/basic-writing-and-formatting-syntax) you can format your comments so that you don't have to use screenshots, > * in the given code, what is the...

So what's the current progress?