Is there a decider for `consistent`

/ `MetaCoq.Template.common.uGraph.gc_consistent`

somewhere?

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: Jun 10 2023 at 06:31 UTC