CoolFace
Datasetpublic

ReactorJet/Coq-Iris

Coq-Iris Structured dataset from Iris, a higher-order concurrent separation logic framework for Coq. Schema Column Type Description fact string Declaration body type string Lemma, Definition, Class, Global, Local, etc. library string Module (iris, iris_heap_lang, iris_unstable, etc.) imports list Require/Import statements filename string Source file path symbolic_name string Declaration identifier Statistics By… See the full description on the dataset page: https://huggingface.co/datasets/ReactorJet/Coq-Iris.

sourceHugging Facebsd-3-clauseupdated 6mo agoView on Hugging Face
0likes8downloads
discussions and pull requests

Conversations for this repository live on Hugging Face.

CoolFace shows imported repositories read-only. Posting into someone else’s repository from here would need an authorised integration and the account holder’s consent, so the link goes to the source instead.

Open discussions on Hugging Face