Coq-FreeSpec – Dataset by phanerozoic | AlphaNeural AI

You can deploy this model and start earning money today!

phanerozoic/
Coq-FreeSpec

like

0

text-generation

feature-extraction

theorem-proving

Views

No views yet

Coq-FreeSpec

Structured dataset from FreeSpec — Modular verification of effectful programs.

Source

Repository: https://github.com/lthms/FreeSpec Commit: d4e2f3a3fc7e82effddca202a8b0210dbbcf3663 Files: 28 License: mpl-2.0

	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… See the full description on the dataset page: https://huggingface.co/datasets/phanerozoic/Coq-FreeSpec.