Is there an easy way to "export" a gallina proof term that was generated by ltac, so that it can be reused as a definition? Using the term printed by
Coq Print does not seem to print valid syntax.
Print foo is usually valid syntax, unless somebody adds bad printing only notation
If that happens, you can disable notations as a workaround (the way depends on the IDE), but you should probably fix those notations.
It might also be a bug? Hard to say
I know you can also have issues with implicit arguments which cannot [always|completely] be inferred from the remaining arguments when it comes to reusing Coq-printed terms; that can also be worked around by setting the flag to print implicit arguments
Thanks! Now the problem is that for very large proofs, it will print
... for sub-terms. I found
Printing Depth, but apparently it has a maximum, which is not enough. Any suggestions how to work around that?
the only reliable way I know of to get terms out from Coq is SerAPI: https://github.com/ejgallego/coq-serapi
Last updated: Oct 03 2023 at 04:02 UTC