yiyuan-cao (Jun 27 2023 at 03:10): yiyuan-cao (Jun 27 2023 at 03:10):Can you please provide high-level insights into how Coq internally implements partial proof terms for tactics such as rewrite,inversion, or induction? Additionally, I would greatly appreciate any references to relevant documentation or research papers on this subject. Thank you in advance for your help!
Notification Bot (Jun 27 2023 at 06:08):This topic was moved here from #Coq users > tactic implementation by Karl Palmskog.
Karl Palmskog (Jun 27 2023 at 09:35):Tactic engine overview by Spiwack: https://github.com/aspiwack/tacengine/releases/download/v0.1-draft/tacengine.pdf
Last updated: Nov 29 2023 at 21:01 UTC