似乎在 Coq 更新 8.18 之后，直接对着本文跑会出现奇怪的问题。原因大概这个方法会装两个 coq-prover，分别来源于 opam 和 snap，这两个 prover 是用两个版本的 OCaml 编译的。可能的解决方法有两个：
因为此文章过于久远，我们建议您不要阅读此文章或者邮件联系作者。
Abstract. 是谁没有 Mac 也没装 Linux 就来选 Software Fundations 啊🤣👉
原来是我🤡🤡🤡
讲一下今晚上配置 coq 环境的流程以及踩的所有坑。其实可能有的地方记不太清楚了。
配置时间和环境：2024. 2. 22，本地环境为 Windows 11 22621.3155，vscode 1.86.2，wsl 发行版为 Ubuntu 22.04，但是感觉未必需要对着配置。
Keywords. 环境配置, wsl, WSL_E_CONSOLE, Coq, VsCoq, opam。
Abstract. 最不想学 FP 的一集《三句话让我写了一晚上形式化验证》。
本文讲如何在 Agda 中定义《数理逻辑与集合论 (1) 命题逻辑》中提到的演绎系统，并形式化验证了文中的几个定理。
好像现在我们的姿势还不太正确，我们确实找到了一种方法来验证一个证明对不对，但是对自己证明定理没有一点帮助（甚至有负贡献）。
Abstract. 从语义的角度来看谓词逻辑，对应书上的第四、第五章。因为听说 thu 没学 6789 章，猜测可能是难度比较大，故在这里断章。
Abstract. 命题逻辑相关的内容，跳过了众所周知的内容，写一些以前没见过的。
第一节主要从语义角度讨论命题逻辑的等值和推理，第二节从语法角度讨论命题逻辑的公理系统，以完备性（和可靠性，但是这里没写）作为连接两者的桥梁。在开头简单阐释一下语义和语法的概念：语义意义下任何等值的变换都可以接受，语法意义下只有变换规则给出的变换可以接受。
参考资料是 thu 的数理逻辑与集合论教材。
Abstract. 在上一节的基础上继续讨论一些通信过程的性质。
Abstract. 本节考虑下图所示的通信模型，对 source 和 channel 部分进行建模，并给出几个与 source 的特性和 channel 的承载率相关的定理（Kraft Inequality，Gibbs Inequality，Source Coding Theorem，Noise Channel Theorem）。
Abstract. 写 Agda 大作业的时候遇到的傻逼问题，解决过程中用到了一些深刻的东西。感觉搞清楚之后对 Pattern Matching 的理解提高了一些。
Abstract. 高等数学复习笔记，参考资料是李忠, 周建莹. 高等数学（上）。