Lean

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

Disclaimer：本文作者还 too young, too simple, sometimes naive，请读者 feel free 跳过第一部分的暴论。