Stream: Coq users

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 to #Coq devs & plugin devs > tactic implementation by Karl Palmskog.

Last updated: Jun 13 2024 at 21:01 UTC