search

UniFormal / MMT

The MMT Language and System
https://uniformal.github.io/
Other
68 stars 23 forks source link

Structure.isInclude neither accounting for implicit morphisms nor for included morphisms #453

Open ComFreek opened 5 years ago

ComFreek commented 5 years ago

Structure.isInclude looks as follows: https://github.com/UniFormal/MMT/blob/13ad1957bd7b3bc56c0242c08c30f5ed0d0643ad/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/Structure.scala#L25

However, Include.unapply does yet neither account for implicit morphisms nor for inclusions of morphisms in views: https://github.com/UniFormal/MMT/blob/13ad1957bd7b3bc56c0242c08c30f5ed0d0643ad/src/mmt-api/src/main/info/kwarc/mmt/api/symbols/Structure.scala#L115-L122

Is there any documentation on how non-trivial inclusions as mentioned above are represented in MMT?