和我签订契约,成为函数式魔法少女吧!
——胡振江(伪) in 《函数式魔法少女》

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

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

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

烧脑环节开始了!

Agda,启动!

参考资料:

《函数式程序设计》课件

《Verified Programming in Agda》

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

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

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