Jason Gross (Nov 02 2022 at 19:32): 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 *))
Meven Lennon-Bertrand (Nov 07 2022 at 14:17):I guess so, yes!
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
Jason Gross (Nov 07 2022 at 23:08):https://github.com/MetaCoq/metacoq/pull/786
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