Jason Gross (Jun 27 2020 at 20:32): 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.
Jason Gross (Jun 27 2020 at 21:00):reported at https://github.com/coq/coq/issues/12600
Last updated: Jun 09 2023 at 04:01 UTC