Stream: MetaCoq

Topic: Checking universe graph?


view this post on Zulip Jason Gross (Oct 26 2022 at 13:23):

Is there a decider for consistent / MetaCoq.Template.common.uGraph.gc_consistent somewhere?

view this post on Zulip 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?)

view this post on Zulip 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