Notification Bot (Aug 23 2022 at 18:22): Notification Bot (Aug 23 2022 at 18:22):Malcolm Sharpe has marked this topic as resolved.
Gaëtan Gilbert (Aug 23 2022 at 19:51):inferring the return clause of matches is complicated
inferring universes with cumulativity is also complicated
Gaëtan Gilbert (Aug 23 2022 at 19:52):btw you can also do if b return Set then bool else bool instead of a cast
Gaëtan Gilbert (Aug 23 2022 at 19:53):see also https://github.com/coq/coq/issues/16068
Last updated: Jan 29 2023 at 06:02 UTC