From cb7bbfd695568dc0a986616928f85dd5aea2a9e7 Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Fri, 13 Nov 2020 18:01:09 +0100
Subject: [PATCH] work
---
.../$Default$Situation$Space.omdoc.xz | Bin 0 -> 580 bytes
.../mmt-omdoc/DefaultSituationSpace.mmt.err | 0
narration/DefaultSituationSpace.omdoc | 2 +
relational/DefaultSituationSpace.rel | 2 +
.../frameworld/$Default$Situation$Space.rel | 8 ++
source/DefaultSituationSpace.mmt | 11 +++
source/IntegrationTests/SituationTheory.mmt | 6 +-
source/examples/misc.mmt | 81 ------------------
8 files changed, 28 insertions(+), 82 deletions(-)
create mode 100644 content/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.omdoc.xz
create mode 100644 errors/mmt-omdoc/DefaultSituationSpace.mmt.err
create mode 100644 narration/DefaultSituationSpace.omdoc
create mode 100644 relational/DefaultSituationSpace.rel
create mode 100644 relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
create mode 100644 source/DefaultSituationSpace.mmt
delete mode 100644 source/examples/misc.mmt
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
new file mode 100644
index 0000000000000000000000000000000000000000..bd614b70d5e5f6096c4d925332ff03922e454b9e
GIT binary patch
literal 580
zcmV-K0=xbFH+ooF000E$*0e?f03iVu0001VFXf})3XK8*T>u^%$);Gjm;(V8!D4R=
zvOFp-REWkEE1f>j;I%&DeXXhUOC=fH*0Ejij1i?$h>zE3%J*;?T3^ss2<$DwDDq;t
znLacvhoKF}xhy$|f6$VZ#Ov`reBZ>@hfo`<QxzlNq}IB1nfqNV0B0|(X-@)8wtOuU
zAiIr_Y~wnskUo>(0Vpv-`jvp~=;;m|;mGSw95p!FL0+9x;V93v1^c9>1ZT)83T)x2
ziCE7$FjlD|34tGZd2NJvr3=|DMTz9G!MNV7T&{&71`huMTcz_TjJ#+<9UUZ%i73eA
z>GCNI@_yb4z)vX!FxKJ$83@Bg*CGZiiU9!J%dG8XHO%RDfilRO^k!(!+<C(o`m+jN
zN;<XRetodUXYd$jM1D835_-T0)eMIRXTaiu?%b@9OT1;`Rvyuu-m&(+fU61nV;-ZK
zoNF~csKVn(8?d8wX@!V{|IvHcVnJXeXY%0WWIS-wDmw)fM&f<F<f0cxId?}J-nY8s
zAE~O)djav3|2u)wcdT*oN+!;LjwHPe=y_T4FzZz=J5`$ByA=Q@{KMZtS)_rUP^D`(
zC$f2qw8kg1cs`c`(X~A6YBII(Z5qaR-zh#SC%WIR5n50JSE(s;{)XhqOKO;_lRYe}
zZvbVQlZ`bqOO3f7V(FCh!jYkOwqGO`c#kAI_QRe40000Lv*OBkK7P~y0i6Vn6#xJe
S*G7P`#Ao{g000001X)^B^AI)w
literal 0
HcmV?d00001
diff --git a/errors/mmt-omdoc/DefaultSituationSpace.mmt.err b/errors/mmt-omdoc/DefaultSituationSpace.mmt.err
new file mode 100644
index 0000000..e69de29
diff --git a/narration/DefaultSituationSpace.omdoc b/narration/DefaultSituationSpace.omdoc
new file mode 100644
index 0000000..774145b
--- /dev/null
+++ b/narration/DefaultSituationSpace.omdoc
@@ -0,0 +1,2 @@
+<?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
diff --git a/relational/DefaultSituationSpace.rel b/relational/DefaultSituationSpace.rel
new file mode 100644
index 0000000..9fa3f6a
--- /dev/null
+++ b/relational/DefaultSituationSpace.rel
@@ -0,0 +1,2 @@
+document http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc
+Declares http://mathhub.info/FrameIT/frameworld/DefaultSituationSpace.omdoc http://mathhub.info/FrameIT/frameworld?DefaultSituationSpace
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
new file mode 100644
index 0000000..a9965ba
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/$Default$Situation$Space.rel
@@ -0,0 +1,8 @@
+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
diff --git a/source/DefaultSituationSpace.mmt b/source/DefaultSituationSpace.mmt
new file mode 100644
index 0000000..f666431
--- /dev/null
+++ b/source/DefaultSituationSpace.mmt
@@ -0,0 +1,11 @@
+namespace http://mathhub.info/FrameIT/frameworld âš
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
+
+theory DefaultSituationSpace =
+ theory Root =
+ include ?OppositeLen â™
+ include ?AngleSum â™
+ include ?Midpoint â™
+ âš
+âš
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index bc4e894..4258dc0 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/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
diff --git a/source/examples/misc.mmt b/source/examples/misc.mmt
deleted file mode 100644
index 748ee87..0000000
--- a/source/examples/misc.mmt
+++ /dev/null
@@ -1,81 +0,0 @@
-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"}
- ]
- }
- }â™
-âš
--
GitLab