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.
subtraction und subtract kollidieren
Wenn ich eine theory habe , die sowohl AllSets von typed_sets.mmt als auch RealArithmetics von reals.mmt importiert , kollidieren die Notationen von subtract (set difference) und subtraction (minus von reals).
Wenn ich die Funktion subtraction direkt verwende (also nicht die notation sondern “subtraction a b”) kann MMT den Typ nicht inferieren… (kommt glaube ich mit dem Subtyping durcheinander). Typanotationen helfen leider auch nicht …
Oh, das ist interessant, das sollte nicht passieren… aber im syntax tree (in jEdit → Sidekick, normalerweise links) taucht auch das richtige subtraction auf? Dann muss ich mir das anschauen, das klingt nach nem tatsächlichen bug…
ist das irgendwo gepusht?
Also wenn ich die Notation für Minus verwende , “-” , dann wird eben fälschlicherweise subtract (von typed_sets) verwendet. Und das steht auch so im sidekick (also, dass subract verwendet wird ). Die Fehlermeldung versteh ich in diesem Fall auch nur so halb (klingt so, als ob aus einem Element vom Typ R ein set R oder so versucht wird abzuleiten).
Wenn ich explizit “subtraction” hinschreibe , steht im sidekick nur “unknown” (und dann wird da eben irgendwas von lambda erzählt). Auch wenn ich nur RealArithmetics importiere geht subraction nicht (die notation “-” wird dafür dann richtig erkannt).
Ich habe ein extra File mit dem Bug angelegt (der Fehler sollte unabhängig von meinen Files):
https://gl.mathhub.info/MitM/smglom/blob/Sven/source/Buggy.mmt
BTW: Wie baut man die Files permanent (das Problem ist, dass der Fehler in einer Theorie ist, die ca. von sieben anderen abhängt, und bisher klicke ich da einfach immer durch , deswegen das extra bugfile für dich).
Das Problem trat ursprünglich hier auf : https://gl.mathhub.info/MitM/smglom/blob/Sven/source/measures/LebesgueIntegral.mmt (beim lebesgueIntegral ca. Zeile 67)
Aber wie gesagt, da muss man vorher ein paar andere theories klicken , damit die “baut” : measures , finiteSet , SetSum, supremum, topology, topologyInstances,
setalgebras,simpleFunctions (in dieser Reihenfolge sollte es klappen) … hoffe ich habe da jetzt nichts vergessen … und dann kann man LebesgueIntegral “bauen” …
Und ja, ist vielleicht alles noch etwas wirr …
Sorry , fall ich einfach nur blind war und was übersehen habe …