Jason Gross (Apr 28 2023 at 07:08): 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: Nov 29 2023 at 22:01 UTC