Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
“role abbreviation”
topology.mmt (und auch eines meiner Files) wirft Fehler , wenn “role abbreviation” in Zeile 20 stehen gelassen wird :
" topology = [X : type] Mod `?OpenSetTopology/topology_theory , X ❘ role abbreviation❙"
Wenn ich dieses abbreviation entferne geht alles. Stimmt da was nicht (bei mir ) ? Das Plugin “extension info.kwarc.mmt.odk.Plugin” hab ich auch an … daran liegt es also nicht … (hab es auch ohne probiert).
Und was macht dieses “role abbreviation” eigentlich ?