What does the ref keyword in MMT do?
I encountered it at the MMT/LATIN2 archive in modal.mmt:
ref latin:/?DisjunctionHilbert2ND❚
ref latin:/?NegationHilbert2ND❚
ref latin:/?ImplicationHilbert2ND❚
ref latin:/?EquivalenceHilbert2ND❚
theory KripkeFrame : latin:/?TypedLogic =
include ?Worlds❙
accessible : tm W ⟶ tm W ⟶ prop❘ # 1 acc 2 prec 30❙
❚
.mmt files get converted into several OMDoc files by MMT, governing three dimensions:
See respective folders in any MMT archive.
content contains information like "this theory contains this constant, which has this type and this definiens", etc. With respect to content, ref does nothing at all.
relational only stores information like "this archive declares this theory", "this theory includes that theory" or "this view has this theory as domain and that theory as codomain". It's something MMT can "quickly" look up at when it wants to know what content exists (and doesn't need all details). If it didn't exist, MMT would need to look up all queries in content files, which would be a lot slower. With respect to relational, again ref does nothing at all.
And finally, there is narration, which contains how (and which) content is declared in which .mmt file. Normally, every .mmt file generates exactly one narration-OMDoc-file and several content-OMDoc-files (one for each theory). The narration-OMDoc also contains things like semantic comments (starting with /t), sectioning, and the precise order in which theories are declared. Narration-OMDoc files can be e.g. inspected in the MMT-server or on MathHub, where they are akin to "active documents" — a nice example is this one: https://mmt.mathhub.info/?http://docs.omdoc.org/examples/tutorial/0-Tutorial.omdoc (note all the comments and explanations)
Now what ref <URI> does is that it "includes" the referenced theory into the current document such that it will be included in the narration-OMDoc-file — without duplicating it in the content dimension. The tutorial file linked above does that occasionally for didactic purposes.