We can extract to a file in Coq with something like:
Extraction "path/to/file" GallinaTerm.
Is there a way to pass in the name of the file programmatically? So that it can be used in a script or something?
Last updated: Oct 13 2024 at 01:02 UTC