Stream: MetaCoq

Topic: ✔ Template.TypingWf.on_option


view this post on Zulip Jason Gross (Nov 02 2022 at 19:32):

Should Template.TypingWf.on_option be replaced by MCOption.on_Some_or_None? (There's a (* TODO MOVE *))

view this post on Zulip Meven Lennon-Bertrand (Nov 07 2022 at 14:17):

I guess so, yes!

view this post on Zulip Jason Gross (Nov 07 2022 at 20:21):

Urgh, I guess on_Some_or_None returns a Prop, we need one that returns a Type here

view this post on Zulip Jason Gross (Nov 07 2022 at 23:08):

https://github.com/MetaCoq/metacoq/pull/786

view this post on Zulip Notification Bot (Nov 07 2022 at 23:08):

Jason Gross has marked this topic as resolved.


Last updated: May 31 2023 at 04:01 UTC