phanerozoic/

Coq-Iris

Structured dataset from Iris, a higher-order concurrent separation logic framework for Coq.

Repository: https://gitlab.mpi-sws.org/iris/iris Commit: 49cc21a1d9be19176b8546a5c5cb0076bf7b14e6 Files: 214 License: bsd-3-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-Iris.