Stream: MetaCoq

Topic: Non-squashed typing judgments?

view this post on Zulip Jason Gross (Oct 23 2022 at 10:52):

It seems that some parts of a typing judgment are not inspectable when my goal is a Type rather than a Prop. (The first such instance is the proof of Universes.LevelSet.Raw.bst, but I expect there may be others.) This is a problem when I'm trying to quote typing judgments from within Gallina. Is there any hope for a "HoTT-compatible" version of typing judgments, where Prop is not used?

view this post on Zulip Matthieu Sozeau (Nov 23 2022 at 12:27):

Ha, tricky question. I think the bst issue can be resolved by using an equivalent is_bst : t -> bool function

view this post on Zulip Jason Gross (Nov 23 2022 at 13:40):

I've managed to bypass this issue by writing deciders for all the Prop bits. Luckily almost everything is either already in Type or easily decidable, with only one exception. (Unfortunately some of the deciders require funext, but that's a separate issue.)

Last updated: Feb 04 2023 at 02:03 UTC