Re: proving _anything_ in the Coq proof assistant (in addition to code execution). « coqchk » passes too

Posted by Georgi Guninski on May 03

10x.

what about this scenario, is it reallistic:

i claim i have a proof of X. the proof is thousands of files.
lambda.v is the plugin and coqc is invoked on only top.v ?

Source: Re: proving _anything_ in the Coq proof assistant (in addition to code execution). « coqchk » passes too