Skip to content
Snippets Groups Projects
Commit 67ee16e1 authored by ComFreek's avatar ComFreek
Browse files

rebuild and ocomment out non-working gearbox theories

parent b2cf9347
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 30 additions and 207 deletions
content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz
+ 0
− 0
View file @ 67ee16e1
No preview for this file type
content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz
+ 0
− 0
View file @ 67ee16e1
No preview for this file type
content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz
+ 0
− 0
View file @ 67ee16e1
No preview for this file type
errors/mmt-omdoc/Library/gearbox.mmt.err
+ 20
− 160
View file @ 67ee16e1
......@@ -56,11 +56,11 @@
<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>
<element>FastREPLExtension.handleLine(REPL.scala:70)</element>
<element>FastREPLExtension.run(REPL.scala:49)</element>
<element>FastREPL$.run(REPL.scala:38)</element>
<element>Test.main(preamble.scala:68)</element>
<element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦y.radius≠0" level="1">
......@@ -121,11 +121,11 @@
<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>
<element>FastREPLExtension.handleLine(REPL.scala:70)</element>
<element>FastREPLExtension.run(REPL.scala:49)</element>
<element>FastREPL$.run(REPL.scala:38)</element>
<element>Test.main(preamble.scala:68)</element>
<element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦x.radius≠0" level="1">
......@@ -186,11 +186,11 @@
<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>
<element>FastREPLExtension.handleLine(REPL.scala:70)</element>
<element>FastREPLExtension.run(REPL.scala:49)</element>
<element>FastREPL$.run(REPL.scala:38)</element>
<element>Test.main(preamble.scala:68)</element>
<element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦RC.radius≠0" level="1">
......@@ -250,151 +250,11 @@
<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>
<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.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?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.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>
<element>FastREPLExtension.handleLine(REPL.scala:70)</element>
<element>FastREPLExtension.run(REPL.scala:49)</element>
<element>FastREPL$.run(REPL.scala:38)</element>
<element>Test.main(preamble.scala:68)</element>
<element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
</errors>
narration/Library/gearbox.omdoc
+ 1
− 1
View file @ 67ee16e1
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2550.72.68"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb2]" target="http://mathhub.info/LoViVo/gearbox?gb2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#1897.53.0:1906.53.9"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb3]" target="http://mathhub.info/LoViVo/gearbox?gb3"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#2448.67.0:2457.67.9"/></metadata></mref></omdoc>
\ No newline at end of file
<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2736.75.68"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><instruction text="namespace http://mathhub.info/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
narration/Scrolls/TriangleScrolls.omdoc
+ 1
− 1
View file @ 67ee16e1
<?xml version="1.0" encoding="UTF-8"?>
<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4945.141.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4919.141.3"/><meta property="http://cds.omdoc.org/?metadata?importedby"><om:OMOBJ xmlns:om="http://www.openmath.org/OpenMath"><om:OMLIT type="http://www.openmath.org/cd?OpenMath?OMSTR" value="mmt-omdoc"/></om:OMOBJ></meta></metadata><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><instruction text="namespace http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
B
/|
/ |
......
relational/Library/gearbox.rel
+ 0
− 2
View file @ 67ee16e1
......@@ -2,5 +2,3 @@ document http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?temp
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?cogwheels
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gearbox
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb2
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb3
relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
+ 0
− 38
View file @ 67ee16e1
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c1
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2av
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
theory http://mathhub.info/LoViVo/gearbox?gb2
HasMeta http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gearbox
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?NaturalDeduction
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c1
constant http://mathhub.info/LoViVo/gearbox?gb2?c1
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2
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
......@@ -20,41 +14,9 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://cds.omdoc.
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
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2av
constant http://mathhub.info/LoViVo/gearbox?gb2?c2av
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
constant http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
source/Library/gearbox.mmt
+ 7
− 4
View file @ 67ee16e1
......@@ -51,13 +51,17 @@ coaxial_cogwheels : ⊦ ∀[x] ∀[y] coaxial x y ⇒ x.angular_velocity ≐ y.
// a particular gear box with two cogwheels, one with undefined angular velocity ❚
theory gb2 =
// doesn't fully typecheck (probably because some computation rules, like for sqrt, are missing, overall non-critical errors ❚
// theory gb2 =
include ?gearbox ❙
include ☞base:?NaturalDeduction ❙
// vvv doesn't typecheck ❙
c1 : rotating_cogwheel ❘ = [' center := (⟨0 , 0⟩), radius:=1, numteeth:=10, angle := 0, angular_velocity:=1 '] ❙
c2 : cogwheel ❘ = [' center := (⟨0 , 2⟩), radius:=1, numteeth:=10, angle := 0.05 '] ❙
// should work: ❙
// should work, but doesn't typecheck: ❙
proof_interlocking : ⊦ interlocking c1 c2 ❘ = eq_refl ((c1.radius) + (c2.radius)) ❙
// ...but needs computation rule for sqrt ❙
c2av : ℝ ❘ = compute_av c1 c2 proof_interlocking ❙
......@@ -65,9 +69,8 @@ theory gb2 =
c2avcheat : ℝ ❘ = avc c1 c2 ❙
❚
theory gb3 =
// theory gb3 =
include ?gb2 ❙
❚
// we want to compute an update rule for the angular velocity of c2 ❚
......
source/Scrolls/TriangleScrolls.mmt
+ 1
− 1
View file @ 67ee16e1
......@@ -103,7 +103,7 @@ theory OppositeLen =
// the description verbalizes deducedLineCA, hence must come after its declaration ❙
meta ?MetaAnnotations?label "OppositeLen" ❙
meta ?MetaAnnotations?description s"Given a triangle △${lverb A B C} right-angled at ⊾${lverb C}, the distance ${lverb deducedLineCA} can be computed from the angle at ${lverb angleB} and the distance ${lverb B C}." ❙
meta ?MetaAnnotations?description s"Given a triangle △${lverb A B C} right-angled at ⊾${lverb C}, the opposide side has length ${lverb deducedLineCA} = tan(${lverb angleB}) ⋅ ${lverb B C}." ❙
❚
❚
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment