文件名称：hierarchy-builder:高级命令基于打包的类声明层次结构
文件大小：201KB
文件格式：ZIP
更新时间：2024-04-27 10:38:23
coq mathcomp elpi Prolog
层次构建器 层次构建器（HB）提供了高级命令来声明Coq系统的代数结构层次结构（如果希望使用计算机科学专业术语，则可以定义接口）。 给定一种结构，就可以发展其理论，并且该理论自动适用于该结构的所有示例。 为了方便或向后兼容，还可以声明替代接口，并提供将这些接口链接到层次结构部分的粘合代码。 HB命令按照打包组件的规定编译为Coq模块，节，记录，强制，规范结构实例和符号，这是库的核心。 所有这些复杂性都隐藏在一些概念和一些声明性的Coq命令之后。 例子 From HB Require Import structures. From Coq Require Import ssreflect ZArith. HB.mixin Record IsAddComoid A := { zero : A; add : A -> A -> A; addrA : forall x y z, a