phanerozoic/

Coq-HoTT

Structured dataset of formalizations from the Coq-HoTT library (Homotopy Type Theory in Coq).

Repository: https://github.com/HoTT/Coq-HoTT Commit: b75eadc7cb2bc59dca415bf47662a9290f82dc5f Files: 589 License: bsd-2-clause

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