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

Last updated: Jan 30 2023 at 17:03 UTC