Coq-Certicoq – Dataset by phanerozoic | AlphaNeural AI

You can deploy this model and start earning money today!

phanerozoic/
Coq-Certicoq

like

0

text-generation

feature-extraction

theorem-proving

Views

No views yet

Coq-Certicoq

Structured dataset from CertiCoq — Verified compiler from Gallina to C.

Source

Repository: https://github.com/CertiCoq/certicoq Commit: 803cd697c1aafb90a609fec18313482e484dc17a Files: 151 License: mit

	Schema

Column Type Description

statement string Declaration signature/claim with the leading keyword removed (verbatim slice); the full declaration minus its proof

proof string Verbatim proof/body, empty if the declaration… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-Certicoq.