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...

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

view this post on Zulip Notification Bot (Nov 23 2022 at 13:50):

Jason Gross has marked this topic as resolved.


Last updated: Jul 24 2024 at 12:02 UTC