Paolo Giarrusso (Aug 14 2020 at 13:53): Paolo Giarrusso (Aug 14 2020 at 13:53):Is there a clear reasons why the two aren't equivalent? Because it seems like they should be?
Paolo Giarrusso (Aug 14 2020 at 13:55):OTOH, since (according to the manual) repeat is equivalent to a strategy using sequencing, that equivalence might suffer from sequencing bugs:
https://github.com/coq/coq/issues/10934
Paolo Giarrusso (Aug 14 2020 at 14:14):Oh. For extra fun, that's fixed by going from terms to nested choices:
Time rewrite_strat (repeat (outermost (choice except_0_exist (choice except_0_and except_0_idemp)))). (* [repeat] works correctly *)
Time rewrite_strat (repeat (outermost (terms except_0_exist except_0_and except_0_idemp))). (* [repeat] doesn't actually work *)
So the last can be successfully rewritten to the sensible strategy topdown:
Time rewrite_strat (topdown (choice except_0_exist (choice except_0_and except_0_idemp))).
Last updated: Oct 13 2024 at 01:02 UTC