Stream: Coq devs & plugin devs

Topic: reduction options


view this post on Zulip 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?

view this post on Zulip 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: Jul 13 2024 at 03:01 UTC