C-zar: the declarative proof language for Coq

Voir cette page en français

Where to get it ?

The C-zar declarative proof language for Coq is part of the standard Coq distribution as of version 8.1 .

How to use it ?

As of version 8.2, the Coq Reference manual contains a section about the C-zar language.

What does it look like ?

Please check the file sqrt2.v for an sample.

I need more details !

A detailed description of the declarative proof language is the basis for this article.


Voir cette page en français