spaceloop (Nov 25 2022 at 18:54): spaceloop (Nov 25 2022 at 18:54):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.
Paolo Giarrusso (Nov 26 2022 at 02:23):Print foo is usually valid syntax, unless somebody adds bad printing only notation
Paolo Giarrusso (Nov 26 2022 at 02:25):If that happens, you can disable notations as a workaround (the way depends on the IDE), but you should probably fix those notations.
Paolo Giarrusso (Nov 26 2022 at 02:25):It might also be a bug? Hard to say
Yann Leray (Nov 26 2022 at 03:05):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
spaceloop (Dec 03 2022 at 10:58):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?
Karl Palmskog (Dec 03 2022 at 11:17):the only reliable way I know of to get terms out from Coq is SerAPI: https://github.com/ejgallego/coq-serapi
Last updated: Oct 13 2024 at 01:02 UTC