phanerozoic/Coq-HoTT

Coq-HoTT数据集是从Coq-HoTT仓库中提取的，专注于在Coq证明助手中形式化同伦类型理论。该数据集处理了理论目录中的`.v`文件，以结构化格式提取数学内容。数据集包括`fact`（完整的数学陈述，包括类型、名称和主体）、`imports`（源文件中的Require Import语句）、`filename`（理论目录中的源文件名）、`symbolic_name`（数学对象的标识符）和`__index_level_0__`（数据集的顺序索引）等字段。该数据集适用于形式方法研究、机器学习应用和教育目的。

The Coq-HoTT Dataset is derived from the Coq-HoTT repository, focusing on the formalization of Homotopy Type Theory in the Coq proof assistant. This dataset processes `.v` files from the theories directory to extract mathematical content in a structured format. The dataset includes the following fields: `fact` (the complete mathematical statement, including type, name, and body), `imports` (the Require Import statements from the source file), `filename` (the source file name within the theories directory), `symbolic_name` (the identifier of the mathematical object), and `__index_level_0__` (sequential index for the dataset). This dataset is designed for formal methods research, machine learning applications, and educational purposes.