Verified_まほうしょうじょ_in_Agda-06

和我签订契约，成为函数式魔法少女吧！
——胡振江（伪） in 《函数式魔法少女》

写这个系列博文的目的是整理我在《函数式程序设计》课程中的一些笔记，以及对 Agda 和 Verified Programming 的一些理解。

这篇文章主要介绍了在 Agda 中的 Internal Verification （内生证明）的数据结构，以及相关的“内生证明”思想。

这是“内生证明”的第二篇文章，我们将会讲到 BST 和 B-Tree 的 Internal Verification ，这时我们就会看到 Internal Verification 的一些更加深入的应用。

烧脑环节开始了！

Agda，启动！

参考资料：

提示:阅读本文章可能需要一定的 FP 基础（例如 Haskell），并掌握 Agda Mode 的基本使用方法

本文章含有 Github Copilot 生成的内容，但作者进行了正确性检查，因而文责自负，如有错误的地方欢迎斧正。

先准备一下我们需要用到的布尔型二元关系