Back
Original
Extracting verified C++ from the Rocq theorem prover at Bloomberg
A new extraction system from
Rocq
to
Rocq to