Is there a decider for
Alternatively, is there a way of manufacturing a
ContextSet.t from a
ConstraintSet.t such that it satisfies
uGraph.global_uctx_invariants? (Is this done somewhere in the safe checker already?)
The graph algorithm decides consistent. Forming a ContextSet.t from a ConstraintSet.t is a simple injection but it's hard to say if it will satisfy the invariants, you probably need hypotheses about things being declared etc...
I've managed to figure this one out at https://github.com/JasonGross/metacoq-lob/blob/4222900653a338b2870e933d1b6a5da7a94a2eb7/theories/Template/Decidable/Universes.v#L11 but there's still one decider I can't figure out
Jason Gross has marked this topic as resolved.
Last updated: Feb 27 2024 at 23:01 UTC