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...
Last updated: Feb 04 2023 at 02:03 UTC