Jason Gross (Oct 23 2022 at 10:52): 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?
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
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: May 31 2023 at 04:01 UTC