Gaëtan Gilbert (May 25 2023 at 10:31): Gaëtan Gilbert (May 25 2023 at 10:31):A month ago I made https://github.com/coq/coq/pull/17503 to expose the weak head options of reductions (lazy,cbn) where we already have them in the ocaml code.
I thought it would be easy to get merged but it seems I underestimated the theoretical complexity ;)
What should we do with this?
Janno (May 25 2023 at 14:45):What exactly is it blocked on? Weak head lazy in particular would be amazing for proof automation purposes.
Last updated: Dec 05 2023 at 12:01 UTC