I noticed that the linkinverter, at least in the IntelliJ plugin GUI, does simply nothing (not even throw an exception, at least none which bubbles up to IntelliJ) in some cases with inclusions.
Namely, if T from the commutative square includes another theory besides S, e.g. Other. The following minimal example should cause the failure, albeit I haven't tested this:
theory R =
❚
theory Other =
❚
theory S =
❚
theory T =
include ?R ❙
include ?Other ❙
❚
view phi : R -> S =
❚
Dirty fix: Just manually flatten the inclusion of Other, i.e. replace include ?Other by contents of Other. Repeat until totally flattened.
I noticed that the linkinverter, at least in the IntelliJ plugin GUI, does simply nothing (not even throw an exception, at least none which bubbles up to IntelliJ) in some cases with inclusions.
Namely, if
Tfrom the commutative square includes another theory besidesS, e.g.Other. The following minimal example should cause the failure, albeit I haven't tested this:Dirty fix: Just manually flatten the inclusion of
Other, i.e. replaceinclude ?Otherby contents ofOther. Repeat until totally flattened.