Skip to main content

Normally a proof assistant is used to complete a proof. As a side effect source code may be generated.

References:
Coq