Stream: Coq users

Topic: Log of type checker

João Mendes (Jun 10 2022 at 02:53):

Is there any way of getting a log of type checker? I'd like, for example, to be able to access the history of tactics used in a proof until the final version of it is reached

Paolo Giarrusso (Jun 10 2022 at 19:16):

Is serapi (or pycoq) related to what you need? It lets alectryon access and pretty-print all intermediate goals in a proof

Paolo Giarrusso (Jun 10 2022 at 19:17):

but it's hard to be sure of what you need: what handles tactics isn't a typechecker

Last updated: Oct 01 2023 at 18:01 UTC