Stream: Coq devs & plugin devs

Topic: tactic implementation


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

view this post on Zulip Notification Bot (Jun 27 2023 at 06:08):

This topic was moved here from #Coq users > tactic implementation by Karl Palmskog.

view this post on Zulip 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: Jun 17 2024 at 22:01 UTC