Stream: Coq users

Topic: Testing, but not adding, universe constraints


view this post on Zulip Janno (Nov 30 2020 at 12:48):

How can I test that a certain universe relation is valid without adding it to the global graph? I want to assert "a < b could be a valid constraint". I tried modules, functors, monomorphic sections in modules/functors, module types,.. All of these add the constraint to the global graph even before the module/functor is imported or even instantiated.

view this post on Zulip Janno (Nov 30 2020 at 12:51):

I suppose I have to move the test into its own file, don't I?

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 12:51):

Section Tmp. Polymorphic Constraint a < b. End Tmp.

view this post on Zulip Janno (Nov 30 2020 at 12:52):

Oh, I see.. I am not even sure now why I wanted a module around it. Thanks!

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 12:52):

something with Fail Constraint may also be possible, I haven't fully thought it through

view this post on Zulip Janno (Nov 30 2020 at 12:52):

Fail Constraint will not be equivalent if the universes are currently unrelated, I think.

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 12:53):

you could also Fail Fail Constraint

view this post on Zulip Janno (Nov 30 2020 at 12:53):

Ah, good old double negation! I'll try that :)

view this post on Zulip Gaëtan Gilbert (Nov 30 2020 at 12:54):

I think Polymorphic Constraint has better errors (Fail Fail will say "command has not failed" or some such thing)

view this post on Zulip Janno (Nov 30 2020 at 12:56):

Indeed. I just tried it and that error message is all I get. Polymorphic Constraint it is, then. Thanks again!


Last updated: Jan 29 2023 at 05:03 UTC