Stream: Coq devs & plugin devs

Topic: rewrite_strat orderings?


view this post on Zulip Jason Gross (Apr 28 2023 at 07:08):

Are there any cases in which topdown or bottomup is better (more optimal / requires asymptotically less computation) than lazy or cbv? (cf https://github.com/coq/coq/issues/13703; what I mean more precisely is consider the version of lazy/cbv that replaces the delta-head step with a (repeat-)rewrite-head step, and otherwise walks the expression tree as lazy/cbv do)


Last updated: Jun 23 2024 at 01:02 UTC