Stream: Coq users

Topic: ✔ Show theorem name tactic.


view this post on Zulip Jason Rute (Jul 29 2022 at 18:35):

Is there a tactic like Show Proof. but that tells you the theorem qualid? Similarly is there one which tells you the theorem statement for which you are proving? Obviously these are not normal requests as this information is visible to the user. This is for data extraction inside Serapi. (In Lean I know how to easily write a tactic to get this data, but not in Coq.)

view this post on Zulip Li-yao (Jul 29 2022 at 18:45):

Show Conjectures.

view this post on Zulip Notification Bot (Jul 29 2022 at 19:26):

Jason Rute has marked this topic as resolved.


Last updated: Sep 30 2023 at 06:01 UTC