Jason Rute (Jul 29 2022 at 18:35): 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.)
Li-yao (Jul 29 2022 at 18:45): 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