phanerozoic/Coq-MetaCoq

MetaCoq数据集源自MetaCoq仓库，专注于在Coq证明助手中形式化Coq的元理论。该数据集处理核心理论目录中的.v文件，以结构化格式提取数学内容。这项工作基于Andreas Florath（@florath）在其Coq事实、命题和证明数据集中建立的格式，提供了MetaCoq库的专门视图，特别关注元编程构造。数据集包括多个字段，如事实、类型、库、导入、文件名、符号名称和索引级别。数据集生成使用了自定义的Python脚本，特别处理了MetaCoq特定的构造。数据集覆盖了多个MetaCoq目录，适用于元理论研究、机器学习应用、元编程研究、认证编程和教育目的。数据集遵循MIT许可证。

The MetaCoq Dataset is derived from the MetaCoq repository, focusing on the formalization of Coqs meta-theory in the Coq proof assistant. This dataset processes .v files from the core theory directories to extract mathematical content in a structured format. It includes fields such as fact, type, library, imports, filename, symbolic_name, and index_level. The dataset is designed for various applications including meta-theoretical research, machine learning, meta-programming studies, certified programming, and educational purposes. It is distributed under the MIT license.