How to handle circular dependency in module import?

Question

I have a module, Reflexive, that imports a module Irreflexive:

module Reflexive
open Irreflexive

The module, Irreflexive, imports the module Reflexive:

module Irreflexive
open Reflexive

That results in this error message:

Circular dependency in module import.

I really do want a reflexive module that imports the irreflexive module (the complement of a relexive relation is irreflexive).

And I really do want an irreflexive module that imports the reflexive module (the complement of an irreflexive relation is reflexive).

Is there any way to handle this circular dependency without merging everything into one module?

Answer 1

A straightforward solution to your problem is to declare a third module in which all predicates/functions/facts needing both reflexive and irreflexive concepts at the same time are declared (e.g. complements as you mentioned). This module could then open both the Reflexive and Irreflexive module without any circular dependency.