编辑于 2023/08

新增夜间模式

编辑于 2022/09

再次将老旧文章移动到 /legacy 目录下，现在这些文章仅可通过 URL 访问，且不会出现在 Posts 列表中。

编辑于 2021/09

距离上次书写博客已经过去了大概 4 个月，期间一直像把这段时间学习到的东西写下来，但一直因为懒而被无限搁置了。

我仔细思考了我为什么当初会选择开设自己的博客，是因为：

• 我希望书写一些网上找不到的东西来满足自己的成就感
• 我希望发表自己的一些作品（小说、散文）和一些经历
• 我希望让自己未来能记住此时的悲欢
• 我希望将自己学会的知识用自己的语言叙述出去，以证明我是真的理解而不仅仅只是对知识的文字描述眼熟
• 我希望自己的一些想法和学习过程中的笔记可以被留下了以便后续查阅
• 我希望可以帮助到后来者，让后来者能更快的入手一个新的技术、新的知识甚至新的想法

今天把博客的首页样式大改了一番并且删除了很多我觉得不符合我写博客的初心的文章。 其中包括很多之前参加英语竞赛时留下的作文，现在看来都是毫无营养的应试作文，没有帮助作用； 还包括一些我觉得已经是人人的常识而不需要过多文字解释的技术型文章； 还包括这个博客系统初始化时留下的 Hello World...

总结

今后的博客更多偏向于技术性总结和技术细节的平民化解释，为了写博客而写博客是毫无疑义的，可惜的是我现在才意识到这个问题。曾经我的博客灌水内容很多，经过今天的整顿和未来的细心维护后，应该可以变成一个对大家有帮助的地方。

Style Demo

Reference: https://plfa.github.io/Inference/ (opens new window)

We first consider the code for synthesis:

synthesize : ∀ (Γ : Context) (M : Term⁺)
           → Dec (∃[ A ] Γ ⊢ M ↑ A )

inherit : ∀ (Γ : Context) (M : Term⁻) (A : Type)
  → Dec (Γ ⊢ M ↓ A)

synthesize Γ (` x) with lookup Γ x
... | no  ¬∃              =  no  (λ{ ⟨ A , ⊢` ∋x ⟩ → ¬∃ ⟨ A , ∋x ⟩ })
... | yes ⟨ A , ∋x ⟩      =  yes ⟨ A , ⊢` ∋x ⟩
synthesize Γ (M ↓ A) with inherit Γ M A
... | no  ¬⊢M             =  no  (λ{ ⟨ _ , ⊢↓ ⊢M ⟩  →  ¬⊢M ⊢M })
... | yes ⊢M              =  yes ⟨ A , ⊢↓ ⊢M ⟩

There are three cases (inline $\KaTeX$):

• If the term is a variable $`x$, we use lookup as defined above:
• If the term is a switch $M ↓ A$ from synthesised to inherited, we recurse on the subterm $M$, supplying type $A$ by inheritance.

There are three cases (inline code):

• If the term is a variable x, we use lookup as defined above:
• If the term is a switch M ↓ A from synthesised to inherited, we recurse on the subterm M, supplying type A by inheritance.

There's an example check (inherit) rule:

$$\Gamma, x : A \vdash t \Leftarrow B \over \Gamma\vdash (\lambda x. t) \Leftarrow A \rightarrow B$$

There's another example:

$$P_{N-1 + m} = \frac{C}{N-{1} + m} \binom{N_{2} - N_{1}}{m}\, \alpha^{m}\beta^{(N_{2} - N_{1}) -m}$$

Some special characters:

$$\mathbb{N}, \mathbb{Z}, \mathbb{R}, \mathbb{C}, \mathbb{I}, \mathbb{F},$$