work

narration/DefaultSituationSpace.omdoc

+<?xml version="1.0" encoding="UTF-8"?>
+<omdoc base="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#0.0.0:259.10.0"/><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/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace]" target="http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.mmt#117.4.0:144.4.27"/></metadata></mref></omdoc>
\ No newline at end of file

relational/DefaultSituationSpace.rel

+document http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace

relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel

+theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace
+HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace?Root
+theory http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root
+HasMeta http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
+Includes http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace/Root http://mathhub.info/FrameIT/frameworld?Midpoint

source/DefaultSituationSpace.mmt

+namespace http://mathhub.info/FrameIT/frameworld ❚
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta ❚
+
+theory DefaultSituationSpace =
+    theory Root =
+        include ?OppositeLen ❙
+        include ?AngleSum ❙
+        include ?Midpoint ❙
+    ❚
+❚

source/IntegrationTests/SituationTheory.mmt

@@ -75,7 +75,11 @@ theory SituationSpace =
 
   theory PushedOutSituationTheory =
     include ?SituationSpace/RootSituationTheory ❙
-    c: type ❘ = b ❙
+    c: type ❙
     q = p ❙
+
+    view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
+      a = c ❙
+    ❚
   ❚
 ❚
\ No newline at end of file

source/examples/misc.mmt

-namespace http://mathhub.info/FrameIT/frameworld/examples ❚
-
-// theory Examples : http://mathhub.info/FrameIT/frameworld?SituationTheoryMeta =
-  A: point ❘ = ⟨1.0, 2.0, 3.0⟩❙
-  B: point ❘ = ⟨4.0, 5.0, 6.0⟩❙
-
-  // this doesn't typecheck due to an MMT bug -- iirc not even Dennis knows what is going on ❙
-  line_AB: line_type ❘ = lineOf A B ❙
-
-  // The measuring tape gadget should produce this fact ❙
-  measured_distance: ⊦ ( ( d- A B) ≐ 42 ) ❘ = sketch "measured by Unity" ❙
-
-  // Below are JSON representations of the above declarations that serve to help build the Unity side ❙
-
-  // JSON representation for A: {
-             "tp": {
-               "kind": "OMS",
-               "uri": "http://mathhub.info/MitM/core/geometry?3DGeometry?point"
-             },
-             "df": {
-               "kind": "OMA",
-               "applicant": {
-                 "kind": "OMS",
-                 "uri": "http://gl.mathhub.info/MMT/LFX/Sigma?Symbols?Tuple"
-               },
-               "arguments": [
-                 {"kind": "OMF", "float": 1.0},
-                 {"kind": "OMF", "float": 2.0},
-                 {"kind": "OMF", "float": 3.0}
-               ]
-             }
-           } ❙
-
-    // JSON representation of line_AB: {
-         "tp": {
-           "kind": "OMS",
-           "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?line_type",
-         },
-         "df": {
-           "kind": "OMA",
-           "applicant": {
-             "kind": "OMS",
-             "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?lineOf"
-           },
-           "arguments": [
-             {"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?A"},
-             {"kind": "OMS", "uri": "http://mathhub.info/FrameIT/frameworld/examples?Examples?B"},
-           ]
-         }
-       } ❙
-
-  // JSON representation for measured_distance: {
-      "tp": {
-        "kind": "OMA",
-        "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?Logic?ded"},
-        "arguments": [{
-          "kind": "OMA",
-          "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?Logic?eq"},
-          "arguments": [
-            {
-              "kind": "OMA",
-              "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/core/geometry?Geometry/Common?metric"},
-              "arguments": [
-                {"kind": "OMS", "uri": "<uri to situation theory, i.e. Examples here>?A"},
-                {"kind": "OMS", "uri": "<uri to situation theory, i.e. Examples here>?B"}
-              ]
-            },
-            {"kind": "OMF", "float": 42}
-          ],
-        }]
-      },
-      "df": {
-        "kind": "OMA",
-        "applicant": {"kind": "OMS", "uri": "http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch"},
-        "arguments": [
-          {"kind": <copy contents of tp here>},
-          {"kind": "OMSTR", "string": "measured by Unity"}
-        ]
-      }
-    }❙
-❚