Open lunaticabs opened 3 months ago
你忘记翻译 https://www.leanprover.cn/fp-lean-zh/type-classes.html 这页了,在文件夹外面XD