diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz
index 9c66c1d8827d69bec5cab1994b6481b91df448fa..1c89915297d0f0c93a500be2dfb8ac53bc371de4 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz
index 328720d4ae26eed7629d584ae0af17a9865844a7..6ac2ee49375c8383abdbd49ee318db4d60743b62 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz
index cb08c3ba9c512d0bde8aa3017733a4d0a6955240..573f9896c1421f634ac1494671d60babf5df14fa 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz
index a1da71e1cd4e983558e4dd0fd37ca03ba3c043cb..1dab85d3ee6bc225cec52200f51d559371fb9916 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz
index 10aadaf2a36f525cd235e964d8ebadacd1dfeb7e..b15b516a6a69e95b3ad2af0d4069640d2c48f016 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Midpoint.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
index 4be756ef007a97bef120d55489c5a7a911d34bee..1341ea63765389c209fe268c185289f84666526c 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz
index 04cb08e7f6a4ecea9b3cbdcb15ac3718d625b019..4ea3894e65019a57eb005d9ace912af6ad94c32b 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Supplementary$Angles.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz
index 5db37a7de24c8f4345688c7907c8070275eff888..fa7d916ce36a2207784a762a6888625cb71b0248 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz
index c4d82a42ebe37a7ffcbc74cfd5c94a71decd26c3..706e89af9a856dc78aa350410e66c96c8a95b071 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$A.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz
index f7372b2efc222ad5cafc630460f565e28b5dd09d..e75c297b022be80fddfefcfa067d2e425a91e5ff 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Angle$At$B.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz
index e47600f8dd1bc6ccd69e4ec3bc2391e2599c7367..05d7531d0ec6f0f2fac778abfa1a30082bdfc861 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Problem_$Right$Angle$At$C.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz
index 4e43126a28f6b8a774e28318bb46ec7ad4e7f4dd..2d56a5277b71c50cb3c4f67fd8ffcf658ca14efe 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz
index bf799aa2f3e8a517edb06ac3a9cd6f86a60c13af..08fcc4295929f4ab4f7c7c73ea60af68ba5e2f24 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Close$Gaps$Test_$Terms$Notepad.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz
index af556ffde48c05d638f7792af047a03624a81c52..733ad04c42f0fc720bf283e1a3b97879853d6e98 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Codomain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz
index 8be229f0aad56ade0a9f3c7bd5da297525f586bf..8a7089d01ade49a490884818da0dadc9f3ceebd7 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Expected$Type$Test_$Domain.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz
index 091ca60bee6c8c92b5eaa3a9585d101db4d25112..f1560af6c779dd467ad64d6816e2b18e1def73b0 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$My$Scroll.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz
index cf8439ffd70c606df68b7fa050633de785b3b15a..2e51bfa253c2616faf94a00068330c14bbef3f1b 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz
index 4c0358ba63d39bea1bd183ceca4c925f0f898afc..2c7d88a9fc8fc03dce37ca39d2aadeccdb43f02b 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Situation$Space.omdoc.xz differ
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz
index 5ec0c0b94284ec1a9c86268ab5ec644fbf34c70f..eb2ebb70b0fe16878d9da40a13784a12e93c3369 100644
Binary files a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz and b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Theory$Parameter$Bug.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz
index 0fc71ab2fa5d0a4535dd59902705de82a93127c4..160ca55d78a4fa4b3f37af2cbb62b3c4ab1d7579 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/cogwheels.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz
index ba50fbe864b73e22310aaba1f00187681a924cb5..7f416c6aead594fad584456104d1195c93a2c16c 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz
index 12bf50ba08d91874fd0284da5f526dda082809b4..fc8667a1833e2db7d8620e35a7fe1399ebc4b702 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz
index 7ee0b0a12463cf21f49a4d914c45cbe1c976d6b1..d0a790242b7fa63b649ca5a1a57e84dd95e75fd4 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/gearbox.omdoc.xz differ
diff --git a/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz
index a02604512702338913af8d6b93a2dfb590faaa5d..fabc89f483da76ca2092d77ed47dbcb6c09819f2 100644
Binary files a/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz and b/content/http..mathhub.info/LoViVo/gearbox/temp.omdoc.xz differ
diff --git a/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index b9e459801db84a8a9028f81eb261036b28ea96b4..7aceb8167d547b4be4bb249111feb530e3173c43 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -1,15 +1,10 @@
<errors>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?temp?dist?definition: Judgment |- [p1,p2] : (â„×â„)⟶(â„×â„)⟶â„" level="2">
+<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦∃![m]m^2 â‰((Ï€l p2)-Ï€l p1)^2 -((Ï€r p2)-Ï€r p1)^2 " level="1">
<stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
@@ -55,25 +50,25 @@
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type: Judgment |- ⊦∀[x:rotating_cogwheel]∀[y:rotating_cogwheel]interlocking x y⇒(x.angular_velocity)/(x.radius)â‰(-y.angular_velocity)/(y.radius) INHABITABLE" level="2">
+<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦y.radius≠0" level="1">
<stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element>
@@ -120,26 +115,25 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
-
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type: Judgment |- ⊦∀[x:rotating_cogwheel]∀[y:rotating_cogwheel]interlocking x y⇒(x.angular_velocity)/(x.radius)â‰(-y.angular_velocity)/(y.radius) INHABITABLE" level="1">
+<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦x.radius≠0" level="1">
<stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element>
@@ -186,157 +180,25 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
-
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type: Judgment |- ⊦∀[x:rotating_cogwheel]∀[y:rotating_cogwheel]interlocking x y⇒(x.angular_velocity)/(x.radius)â‰(-y.angular_velocity)/(y.radius) INHABITABLE" level="1">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.checkInhabitable$1(MMTStructureChecker.scala:316)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13(MMTStructureChecker.scala:325)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$13$adapted(MMTStructureChecker.scala:322)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:322)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
-
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition: Judgment |- [RC,C,p]-((RC.angular_velocity)/(RC.radius))â‹…C.radius : {RC:rotating_cogwheel,C:cogwheel}⊦interlocking RC C⟶â„" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
-
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition: Judgment |- [RC,C,p]-((RC.angular_velocity)/(RC.radius))â‹…C.radius : {RC:rotating_cogwheel,C:cogwheel}⊦interlocking RC C⟶â„" level="1">
+<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦RC.radius≠0" level="1">
<stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12(RuleBasedChecker.scala:88)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$12$adapted(RuleBasedChecker.scala:85)</element>
<element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
+ <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:85)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
<element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
<element>scala.Option.foreach(Option.scala:407)</element>
@@ -382,14 +244,19 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
-
<error
type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c1?definition: Judgment |- ['center=⟨0,0⟩,radius=1,numteeth=10,angle=0,angular_velocity=1'] : rotating_cogwheel" level="2">
<stacktrace>
@@ -447,266 +314,20 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c2?definition: Judgment |- ['center=⟨0,2⟩,radius=1,numteeth=10,angle=0.05'] : cogwheel" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c2?definition: Judgment |- ['center=⟨0,2⟩,radius=1,numteeth=10,angle=0.05'] : cogwheel" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
- <stacktrace>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element>
- <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element>
- <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element>
- <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element>
- <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element>
- <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element>
- <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element>
- <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element>
- <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element>
- <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element>
- <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element>
- <element>scala.collection.immutable.List.foreach(List.scala:392)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
- </stacktrace>
-</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" level="2">
<stacktrace>
<element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element>
@@ -763,11 +384,17 @@ type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid un
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element>
<element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld$.main(BuildFrameworld.scala:11)</element>
- <element>info.kwarc.mmt.frameit.communication.server.playground.BuildFrameworld.main(BuildFrameworld.scala)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle(ActionHandling.scala:69)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
+ <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
+ <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
+ <element>FastREPL.handleLine(REPL.scala:68)</element>
+ <element>FastREPL.run(REPL.scala:48)</element>
+ <element>REPL$.doFirst(REPL.scala:34)</element>
+ <element>Test.main(preamble.scala:55)</element>
+ <element>REPL.main(REPL.scala)</element>
</stacktrace>
</error>
</errors>
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
index 3aa05d239ee890672ec53103c74d83e0547f72e8..18715a350767df6634ca85bd70e0bd8e1b0146c5 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/cogwheels.rel
@@ -21,9 +21,6 @@ constant http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle
DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/cogwheel_theory?angle?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel
constant http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel_theory
theory http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory
HasMeta http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory http://mathhub.info/MitM/Foundation?Logic
@@ -36,6 +33,3 @@ constant http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory?a
DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels/rotating_cogwheel_theory?angular_force?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?cogwheels http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel
constant http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
index 9eec5e1a8a588435994a704fe7c057710e4aa454..ee58104abfa6e6176a7d8aa8ac9c944767d2b1b2 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
@@ -15,6 +15,11 @@ Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearb
constant http://mathhub.info/LoViVo/gearbox?gb2?c2
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
constant http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?type
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
index ef6aadb1478ef6a41dbc6ec2145e273b07acd2ef..ab1cc4ea28333b1564238a5e4f20d5123f19a223 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gearbox.rel
@@ -18,6 +18,24 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition htt
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels
constant http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?neq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/core/arithmetics?RealArithmetics?div?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?neq?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?forall?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?interlocking_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?gearbox http://mathhub.info/LoViVo/gearbox?gearbox?coaxial
constant http://mathhub.info/LoViVo/gearbox?gearbox?coaxial
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial?type http://mathhub.info/MitM/Foundation?Logic?prop?type
@@ -35,11 +53,9 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?implies?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?forall?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?coaxial_cogwheels?type http://mathhub.info/MitM/Foundation?Logic?eq?type
@@ -57,3 +73,17 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://math
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?neq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?div?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?Logic?neq?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?RealLiterals?minus_real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://cds.omdoc.org/urtheories?NatSymbols?NAT?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
index 18ae45a45e9c0e4dd4307e6319d2974d762757da..7b51cc248325726aa705dc2ef42067ee49ec1439 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/temp.rel
@@ -6,3 +6,18 @@ Includes http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/MitM/Founda
Declares http://mathhub.info/LoViVo/gearbox?temp http://mathhub.info/LoViVo/gearbox?temp?dist
constant http://mathhub.info/LoViVo/gearbox?temp?dist
DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?ImplicitProof?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type
+DependsOn http://mathhub.info/LoViVo/gearbox?temp?dist?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type