Stream: Coq devs & plugin devs

Topic: rewrite matching algorithms


view this post on Zulip Jason Gross (Jun 27 2020 at 20:32):

What's the difference between ssr rewrite's matching algorithm and vanilla Coq's? Interestingly, ssr's rewrite ! is linear in the size of the goal when there are no occurrences of the head symbol (and every constant that appears in the goal is either an Axiom or an Inductive), while autorewrite and Coq's rewrite ! are quadratic in the size of the goal. (I'll be reporting an issue about this shortly.

view this post on Zulip Jason Gross (Jun 27 2020 at 21:00):

reported at https://github.com/coq/coq/issues/12600


Last updated: Oct 16 2021 at 02:03 UTC