Jason Gross (Oct 26 2022 at 13:23): Jason Gross (Oct 26 2022 at 13:23):Is there a decider for consistent / MetaCoq.Template.common.uGraph.gc_consistent somewhere?
Jason Gross (Nov 03 2022 at 16:31):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?)
Matthieu Sozeau (Nov 23 2022 at 12:51):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...
Jason Gross (Nov 23 2022 at 13:50):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
Notification Bot (Nov 23 2022 at 13:50):Jason Gross has marked this topic as resolved.
Last updated: Jun 10 2023 at 06:31 UTC