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"}
        ]
      }
    }❙
❚