Clef RFC research
Proposals for the Clef language whose claims are theorems. Each RFC is a Rocq development: the design rules are definitions, and what the design promises is proved from them.
RFCs
| RFC | Title | Stage | Theorems proved | Lemmas proved | Unproved | Own assumptions |
|---|---|---|---|---|---|---|
| 0001 | Closed-set type constraints | Draft | 17 | 11 | 0 | 0 |
A theorem is a claim the RFC makes to its readers, and a lemma is a step toward one. Unproved counts statements that end in Admitted. Own assumptions counts axioms and parameters the RFC declares for itself, beyond the 10 taken from the specification in the shared Spec modules.
What a proof here does and does not show
A proof shows that a claim follows from the model and the assumptions. It does not show that the model matches the compiler, or that an assumption reads the specification correctly. Each RFC says what its model leaves out, and every theorem lists the assumptions its proof used.
This site is research. It is not part of the Clef specification, and nothing here is accepted until it goes through the specification's change process.