diff --git a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class deleted file mode 100644 index 09006ce7f066e2d90cab7fbfe6dc2faf0cfdb992..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible$.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class b/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class deleted file mode 100644 index 26061b5129e9e082e3efb0729c4758b7a6c47d37..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/AngleInvertible.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class b/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class deleted file mode 100644 index 22f05eba9c7947d37268b5687e95557d8623dbd1..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/FrameIT$.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/FrameIT.class b/bin/info/kwarc/mmt/frameit/rules/FrameIT.class deleted file mode 100644 index ab219786521b0d985cff923a92f773524942ad96..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/FrameIT.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class deleted file mode 100644 index 333752ef05c182d3f6d4fd188d63db32054cce68..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative$.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class b/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class deleted file mode 100644 index aaccece7268161e0c6c4b2712c57cbf2a5f54d32..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/MetricCommutative.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/Symbols$.class b/bin/info/kwarc/mmt/frameit/rules/Symbols$.class deleted file mode 100644 index 140f47f69b8fd9810f80ba46a31ad75f13656354..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/Symbols$.class and /dev/null differ diff --git a/bin/info/kwarc/mmt/frameit/rules/Symbols.class b/bin/info/kwarc/mmt/frameit/rules/Symbols.class deleted file mode 100644 index d6d5c179f2bf88e652c9bdd65d9183fe97aabcf6..0000000000000000000000000000000000000000 Binary files a/bin/info/kwarc/mmt/frameit/rules/Symbols.class and /dev/null differ diff --git a/build.msl b/build.msl index bcb8a09cbfba84136b89f0dd11a132f406cb94c0..5caf8d9d572233c29e524400ac4b76cb7780aa4d 100644 --- a/build.msl +++ b/build.msl @@ -1,3 +1,5 @@ build FrameIT/frameworld mmt-omdoc MetaTheories.mmt +build FrameIT/frameworld scala-bin +build FrameIT/frameworld mmt-omdoc dynamics.mmt build FrameIT/frameworld mmt-omdoc Scrolls/ build FrameIT/frameworld mmt-omdoc DefaultSituationSpace.mmt diff --git a/frameworld.iml b/frameworld.iml new file mode 100644 index 0000000000000000000000000000000000000000..2e3968af5181a9fe17ab2fe193be128ab4492794 --- /dev/null +++ b/frameworld.iml @@ -0,0 +1,17 @@ +<?xml version="1.0" encoding="UTF-8"?> +<module type="JAVA_MODULE" version="4"> + <component name="NewModuleRootManager"> + <output url="file://$MODULE_DIR$/bin" /> + <exclude-output /> + <content url="file://$MODULE_DIR$"> + <sourceFolder url="file://$MODULE_DIR$/scala" isTestSource="false" /> + <excludeFolder url="file://$MODULE_DIR$/bin" /> + </content> + <orderEntry type="inheritedJdk" /> + <orderEntry type="sourceFolder" forTests="false" /> + <orderEntry type="module" module-name="mmt-api" /> + <orderEntry type="module" module-name="mmt-lf" /> + <orderEntry type="module" module-name="LFX" /> + <orderEntry type="library" name="scala-sdk-2.13.1" level="application" /> + </component> +</module> \ No newline at end of file diff --git a/source/.idea/source.iml b/source/.idea/source.iml deleted file mode 100644 index d6ebd4805981b8400db3e3291c74a743fef9a824..0000000000000000000000000000000000000000 --- a/source/.idea/source.iml +++ /dev/null @@ -1,9 +0,0 @@ -<?xml version="1.0" encoding="UTF-8"?> -<module type="JAVA_MODULE" version="4"> - <component name="NewModuleRootManager" inherit-compiler-output="true"> - <exclude-output /> - <content url="file://$MODULE_DIR$" /> - <orderEntry type="inheritedJdk" /> - <orderEntry type="sourceFolder" forTests="false" /> - </component> -</module> \ No newline at end of file diff --git a/source/Scrolls/BouncingScroll.mmt b/source/Scrolls/BouncingScroll.mmt index 9439000af011d12dd049d061f775670d34ffd50a..99075e63b5c336ec58f33f8122e112f104acd676 100644 --- a/source/Scrolls/BouncingScroll.mmt +++ b/source/Scrolls/BouncingScroll.mmt @@ -2,16 +2,9 @@ namespace http://mathhub.info/FrameIT/frameworld âš import base http://mathhub.info/MitM/Foundation âš import arith http://mathhub.info/MitM/core/arithmetics âš -//import rules scala://datatypes.LFX.mmt.kwarc.info âš import rules scala://rules.frameit.mmt.kwarc.info âš -//fixmeta base:?Logic âš fixmeta ?FrameworldMeta âš -theory StepUntilWrap = - stepUntil : ℠⟶ (℠⟶ â„) ⟶ (℠⟶ bool) ⟶ List[â„] ☠# stepUntil 1 2 3 â™ - rule rules?StepUntilRule (true) â™ -âš - theory BouncingScroll = meta ?MetaAnnotations?problemTheory ?BouncingScroll/Problem â™ meta ?MetaAnnotations?solutionTheory ?BouncingScroll/Solution â™ diff --git a/source/Scrolls/SupplementaryAngles.mmt b/source/Scrolls/SupplementaryAngles.mmt index 58ccc1813294c28e87fe5bd6bee04dcc3cae30a6..b15e794c75d21c5144db3cfeaa4c70021d1292df 100644 --- a/source/Scrolls/SupplementaryAngles.mmt +++ b/source/Scrolls/SupplementaryAngles.mmt @@ -8,10 +8,10 @@ fixmeta ?FrameworldMeta âš ________\_________ A B C -The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD" +The scroll encodes "angle ABD + angle DBC = 180°", or rather, "angle DBC = 180° - angle ABD". âš theory SupplementaryAngles = - meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem â™ + meta ?MetaAnnotations?problemTheory ?SupplementaryAngles/Problem â™ meta ?MetaAnnotations?solutionTheory ?SupplementaryAngles/Solution â™ theory Problem = diff --git a/source/dynamics.mmt b/source/dynamics.mmt new file mode 100644 index 0000000000000000000000000000000000000000..6e77c20c53534c88c9b1139f95343a6d169a8b3a --- /dev/null +++ b/source/dynamics.mmt @@ -0,0 +1,12 @@ +namespace http://mathhub.info/FrameIT/frameworld âš + +import base http://mathhub.info/MitM/Foundation âš +import arith http://mathhub.info/MitM/core/arithmetics âš +import rules scala://rules.frameit.mmt.kwarc.info âš +fixmeta ?FrameworldMeta âš + +theory StepUntilWrap = + stepUntil: ℠⟶ (℠⟶ â„) ⟶ (℠⟶ bool) ⟶ List[â„] ☠# stepUntil 1 2 3 â™ + rule rules?StepUntilRule (true) â™ +âš +