Stream: CertiCoq

Topic: vm_cast_no_check

Bas Spitters (Feb 26 2021 at 15:27):

Is there a version of this for certicoq?

Andrew Appel (Mar 04 2021 at 13:14):

No. CertiCoq is a plug-in that extracts code to outside of Coq, not integrated into the Coq kernel like vm_compute. Maybe someday in the future, but not this year.

Last updated: Feb 06 2023 at 06:29 UTC