ReactorJet/Coq-Stdlib

---
license: lgpl-2.1
task_categories:
- text-generation
- feature-extraction
language:
- en
tags:
- theorem-proving
- formal-methods
- coq
- standard-library
size_categories:
- 1K<n<10K
dataset_info:
features:
- name: fact
dtype: string
- name: type
dtype: string
- name: library
dtype: string
- name: imports
list: string
- name: filename
dtype: string
- name: symbolic_name
dtype: string
- name: docstring
dtype: string
splits:
- name: train
num_bytes: 692381
num_examples: 2364
download_size: 151271
dataset_size: 692381
configs:
- config_name: default
data_files:
- split: train
path: data/train-*
---

# Coq-Stdlib

Structured dataset of definitions and theorems from the Coq standard library.

## Dataset Description

- **Source:** [coq/coq/theories](https://github.com/coq/coq/tree/master/theories)
- **Entries:** 2,364
- **Files processed:** 106
- **License:** LGPL-2.1 (matches Coq)

## Schema

| Column | Type | Description |
|--------|------|-------------|
| fact | string | Declaration body (without type keyword) |
| type | string | Definition, Lemma, Theorem, Fixpoint, Inductive, Class, Instance, Ltac, Ltac2, etc. |
| library | string | Top-level module (Corelib, Ltac2) |
| imports | list | Require/Import statements |
| filename | string | Source file path |
| symbolic_name | string | Declaration identifier |

## Statistics

### By Type
| Type | Count |
|------|-------|
| Definition | 688 |
| Lemma | 553 |
| Ltac2 | 550 |
| Ltac | 124 |
| Fixpoint | 75 |
| Axiom | 74 |
| Theorem | 62 |
| Class | 48 |
| Inductive | 48 |
| Instance | 45 |

## Use Cases

- Retrieval/RAG for Coq
- Learning Coq standard library patterns
- Training embeddings for formal proofs
- Documentation exploration

## Related Datasets

- [Coq-HoTT](https://huggingface.co/datasets/phanerozoic/Coq-HoTT)
- [Coq-UniMath](https://huggingface.co/datasets/phanerozoic/Coq-UniMath)
- [Coq-MetaCoq](https://huggingface.co/datasets/phanerozoic/Coq-MetaCoq)