Lean

今天学习了一些 Lean 4 里 structure elaborator 的实现， 实际上 structure 比预想的要复杂得多！这里记录一些有趣的现象，没用的知识又增加了.jpg。