Verified_まほうしょうじょ_in_Agda-06
和我签订契约,成为函数式魔法少女吧!
——胡振江(伪) 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 生成的内容,但作者进行了正确性检查,因而文责自负,如有错误的地方欢迎斧正。
先准备一下我们需要用到的布尔型二元关系
本博客所有文章除特别声明外,均采用 CC BY-NC-SA 4.0 许可协议。转载请注明来自 Morgen-Kornblume's Blog!
评论