Stream: Coq users

Topic: ✔ Puzzling error with dependent types


view this post on Zulip Notification Bot (Aug 23 2022 at 18:22):

Malcolm Sharpe has marked this topic as resolved.

view this post on Zulip Gaëtan Gilbert (Aug 23 2022 at 19:51):

inferring the return clause of matches is complicated
inferring universes with cumulativity is also complicated

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

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