Stream: Coq users

Topic: Log of type checker


view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Feb 01 2023 at 11:04 UTC