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.
I suppose I have to move the test into its own file, don't I?
Section Tmp. Polymorphic Constraint a < b. End Tmp.
Oh, I see.. I am not even sure now why I wanted a module around it. Thanks!
something with Fail Constraint may also be possible, I haven't fully thought it through
Fail Constraint will not be equivalent if the universes are currently unrelated, I think.
you could also
Fail Fail Constraint
Ah, good old double negation! I'll try that :)
I think Polymorphic Constraint has better errors (Fail Fail will say "command has not failed" or some such thing)
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