Scribbles

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

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

不知不觉距离更新上篇技术性博客已经过去四个月了！最近一段时间攒起来的想法应该能写出几篇了—— 但是想要系统性地把一些知识讲明白、并且组织成条理分明的文章还是很耗时的，所以就没有投入时间把它们写出来。不过仔细想想，即使是零散的、未成熟的想法也有分享的价值，并且能督促我时常回顾它们。

因此我打算在这个网站开一个新的“小碎片系列”，平行于其他博客文章。它基本上是一个公开的 Obsidian/散装的知识库，包括比较随机多草稿和片段。这些碎片最终会被整理编排成正式的博客文章，大概。此外，这个系列会保持中文（我太久没有用中文写过东西了……）、使用尽量随意的语言、并附带上我的个人想法，而非全部中立的陈述。

总之希望这个决定能增加一些更新频率。目前 Verso 还不支持非英文标题，刚刚提了个 Issue。维护一个 fork 稍微魔改一下不会很困难，不过还是希望能得到官方支持。

顺带一提，这些碎片会在 Atom feed 上和正式博客交替出现，欢迎点击页脚的 Atom 图标订阅！