From 891df92023769e66609f4944faa46dc055592784 Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Sun, 25 Apr 2021 18:59:39 +0200
Subject: [PATCH] document situation spaces
---
README.md | 5 +-
.../$Situation$Space.omdoc.xz | Bin 0 -> 1916 bytes
.../IntegrationTests/SituationTheory.mmt.err | 2 -
.../IntegrationTests/SituationTheory.omdoc | 2 +-
.../IntegrationTests/SituationTheory.rel | 4 +-
.../$Situation$Space.rel | 139 ++++++++++++++++++
situation-space.md | 67 +++++++++
source/IntegrationTests/SituationTheory.mmt | 65 ++++----
source/Scrolls/README.md | 84 +++++------
9 files changed, 285 insertions(+), 83 deletions(-)
create mode 100644 content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz
create mode 100644 relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
create mode 100644 situation-space.md
diff --git a/README.md b/README.md
index c55f205..ad958ab 100644
--- a/README.md
+++ b/README.md
@@ -16,9 +16,10 @@ Besides that, there is also
- [`IntegrationTests/`](./source/IntegrationTests): contains some integration tests run by the unit tests in the frameit-mmt submodule of the UniFormal/MMT project
-## Contributing
+## Documentation
-See [`Scrolls/README.md`](./source/Scrolls) for how to write scrolls.
+- [`./source/Scrolls/README.md`](./source/Scrolls) for a guide on how to write scrolls.
+- [`./situation-space.md`](./situation-space.md) for an overview how a situation space and theory looks like over the course of playing.
## Authors
diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.omdoc.xz
new file mode 100644
index 0000000000000000000000000000000000000000..9eaa82160a954bd1e5527e0b86005f8037e54fb8
GIT binary patch
literal 1916
zcmV-?2ZQ+iH+ooF000E$*0e?f03iVu0001VFXf})h0X^&T>u^%$);Gjm;(V8!D4R=
zvOFp-REWkEE1f>j;I%&DeXXhUOC=fH*0Ejij1i?$h>zE3%J*;?T3^ss2<$DwDDq;t
znLacvhpuSMps+`HW&xnrIE<+PL!-1JqfnvzEJEN?sgF81K9pLA$a-TI$l7_t`NmH0
zZcr<ad+p<1bj!DJK;C5>7nXHGG3zQ2Lf(T%1w(eq-UOCanYk_`IzwYu>St93q5c(_
zh5}!-e>@0j7sfZKJ`;q{kZoroRr*Hm#?=!NqCoMGP~HpWnq!B!14CNJHE2lpco4_?
z)>CPk*%|+vLPy(&%L`7u%vtA}siE=)IZKr63WeTHnU&^v+`8xWT}8crv`A|J32)kq
ze%&%0Vc+ntn6Ap8FW2XPg_m(xERIyj<`C)&6^WVwLf+kNh|b+Jnh4LuVa|JXK=;K<
z4L%QbE!W%jWqi=qgL0^ZEOrEcF11U$)!)b47xvMv0Y?M2RUqT|HTs-y7s9rtw`xIM
zx8CcsHMMn8;qqaB-!i~gooYN6s4rQYxe4AqXL3$HiLTSDxG?JA7Pi=)Xmd?9%P48;
zkp{+c{vP;{yrO|Yk`1zyo*2>TP_baq=3H{kX#yH{dSMsGzZH%>v#|DsYHTNlyhPUA
zI%bGde#a}P^6~eZr_b}1m}1c7kku2fMxcB($tB%zw~pI%&bO$G?N;SKnmW>X4FMlK
zkb*MPUa7Qi#$r(tTe-G2V{s3%BN_CbEd_qiMP38I<Mt@*Z+2_T?z8!^i~RQiBI|S_
zE*z6VImB@2fM2gmi^>65Ds9BH+f$-ur~E@)3Jz(8y3VI7sB=-<N4LdS!8MWU<VHgA
z>R`BhTcH5|uyz34gZgpy9Xq?nFV7<Gc;@#33mk@At%Cln@`<;OvzyvYj*CFQZ0b1Z
z(k6Fl<mpIT?2Woh`?cJzc(;Cw+AvXNsGPcwYf8;j8}B#vn(7lu-x+}D(mP|>T<1F_
zvyPZ9ye5xm4{=V;r|KB}O+>tLpv7g{N|X^=!wTP%E~>j#lga1i3awXrtT76SZETR-
zMw;80ml=e7+=*Am!OTvjsUc1^$G*EQXxk^n3EBrw+(-w7l9ES>U+bOzqQUXyNSz#f
zCNpqHpXBds1BYNEIW|_Qb}Hdx#7?M{^2}dt8*F|pU4*u#3tPI;BD)tyE?fvc0u8zq
zs3JAT#TFD+d>c0QUwn<pim;-}FtzSny@ggaM+CDqTKz9Ge=G!wcGr!4V=+rN3P64e
zVDy5n0cSRO9wh2S=iIWoMAcVs+74}sxi?F9J-P;3cHFhh3UM!|8~8QG&nY_l?TLmS
zkr`f49`gGpoRi19<$THJ{M!QEFd_k526wejhkB_LN;2U~I6Hu!4;18<VYvrYKMmK4
zh$u%W*o2D2xQ*Zo(f8DArCx)^fiOTY`0Bf)i_MPcR_*Qz6br42skHrC^@CVU&o|sC
zlDTh@v)*8_l&Nt1#?dJ4^h)hGxeP6cI^v`3q~24pah*BivQjU21-xFV*agTHd_9);
zT;k&|DI}+)wXm%b-JInZs^{6@D7}sa3V~|O6M0?js(wC|<-D}4O{)3=60nCYS#uVk
zVG2*bcM2NFuh3){Y<-8AB@lrz4aTE8!=^?^K3>;4mQsq?H!(m<Z+zDClTrm$Wlk0v
zHUrOrPs~fHQo8N7x02kmq4O25V1|6v4c2h{S$n^^;wId<#iOYL{g5`wK{`wW9pko=
zc{W4+@-#Ev{!080`$&N{hy#dGh@ig($AV*IK@Fssx5M8JORn^#=orqOl|*%+rXTs}
zjk5bN@k-jj<WWaOUi_F|ls`5Z{Zr5aY@1y!*zrRcToKXWl5w)#K|^Awq)fE(MqP0s
z<sneQnwyWTX#9*asgL+{i`)Me)h7G;4mQ&bvB>n>lOn+h2^jfl6uLpwU2`3wG2+8-
z?ob`SA1+Q}B$omA(r~~e=W5<neEpgNtR=}Mjd3R)1G6nBz&|h-8=rgBPt}Inyk_()
zO8)8<!~75n0#g)G0b-XtHd0-{80LPqrjB38U;Rv`OQ?|y&TfdHlrE_O?%kl8L3sBW
z<`U>|=>3nGqv7wy>KM_q!uv~Vss$^KnT%>+gpW~ucf#cna4_8AbhrrUso%r;Q$~Uo
z0VQ4eJtnRxw~()hEY2Fm=Pj&5IP6+CZ8Vw340ww&%NI8YlvfrcL#oM_pMqVuV_JIk
zt!qU|O1rPJ2jJ%7g$)TSf(@e84xW+wQ;xh5r-&BLOeCB@%mqs6XS&Q>J&gQ<BL6#G
zY8r?ESCI~hw8IEUTc%+Jnh=++CJ%?rD8s~oIdOpAYE1kTpc(XfRYvzn55&zkidL<D
z76PV}b5pCiEg8HfkY_^Qpj_i_d%P{?{?XzWY}6hh%_L35GpIO!AK0u?psfFB&a#Lt
zJtrnqujtNI#bIGSk<5JM)c^n!#fJB2aJ!!X0oV@Divj>moN#lo#Ao{g000001X)^0
CueUt_
literal 0
HcmV?d00001
diff --git a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
index a003a31..e69de29 100644
--- a/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
+++ b/errors/mmt-omdoc/IntegrationTests/SituationTheory.mmt.err
@@ -1,2 +0,0 @@
-<errors>
-</errors>
diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc
index 6d8c720..1b100fc 100644
--- a/narration/IntegrationTests/SituationTheory.omdoc
+++ b/narration/IntegrationTests/SituationTheory.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:2102.84.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/integrationtests"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:220.6.26"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1535.56.0:1549.56.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#1661.64.0:1681.64.20"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#0.0.0:1753.61.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/integrationtests/space_typechecking_test"/><instruction text="rule scala://parser.api.mmt.kwarc.info?MMTURILexer"/><instruction text="import frameworld http://mathhub.info/FrameIT/frameworld"/><instruction text="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace]" target="http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#271.7.0:291.7.20"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/relational/IntegrationTests/SituationTheory.rel b/relational/IntegrationTests/SituationTheory.rel
index 76d8127..9e59fa8 100644
--- a/relational/IntegrationTests/SituationTheory.rel
+++ b/relational/IntegrationTests/SituationTheory.rel
@@ -1,4 +1,2 @@
document http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationSpace
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?MyScroll
-Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests?SituationSpace
+Declares http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.omdoc http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
new file mode 100644
index 0000000..ce0b425
--- /dev/null
+++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test/$Situation$Space.rel
@@ -0,0 +1,139 @@
+theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace?Root
+theory http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
+HasMeta http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?FrameworldMeta
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?OppositeLen
+Includes http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld?AngleSum
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleABC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?angleBAC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Strings?string?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?A?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://cds.omdoc.org/urtheories?Ded?DED?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?C?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?B?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?angle_between?type
+DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?rightAngledC?definition http://mathhub.info/MitM/Foundation?Logic?prop?type
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root?first_view
+HasDomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view ☞frameworld:?OppositeLen/Problem
+HasCodomain http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root
+view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view
+HasViewFrom http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root ☞frameworld:?OppositeLen/Problem
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?A
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?B
+Declares http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
+constant http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test?SituationSpace/Root/first_view?C
diff --git a/situation-space.md b/situation-space.md
new file mode 100644
index 0000000..fff662f
--- /dev/null
+++ b/situation-space.md
@@ -0,0 +1,67 @@
+## The Evolution of a Situation Space
+
+This is an overview of how a situation space and theory looks like over the course of playing.
+
+Read from top to bottom; the comments indicate the "current" action that led to the creation of the respective module or declaration.
+
+```mmt
+
+fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
+
+theory SituationSpace =
+ // Player starts with situation_theory_1 below that includes this root situation theory,
+ providing access to scrolls that are available by default â™
+ theory Root =
+ include ☞http://mathhub.info/FrameIT/frameworld?OppositeLen â™
+ include ☞http://mathhub.info/FrameIT/frameworld?AngleSum â™
+ include ☞http://mathhub.info/FrameIT/frameworld?Midpoint â™
+ âš
+
+ // Player starts with this situation theory. â™
+ theory situation_theory_1 =
+ include ?DefaultSituationSpace/Root â™
+
+ // The player collects some facts about the world. â™
+ fact1: ... â™
+ fact2: ... â™
+ fact3: ... â™
+
+ // The player formulates a scroll view... (continued below) â™
+ view scroll_view_1 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_1 =
+ factslot1 = fact1 â™
+ factslot2 = fact2 â™
+ factslot3 = fact3 â™
+ âš
+ âš
+
+ // (continued)... and applies the scroll and thus lands in a new derived situation theory. â™
+ theory situation_theory_2 =
+ include ?SituationSpace/situation_theory_1 â™
+
+ // The player gets access to facts obtained by the scroll (these are precisely the ones pushed out
+ from ?OppositeLen/Solution over ?SituationSpace?situation_theory_1?scroll_view_1). â™
+ out_fact1: ... â™
+ out_fact2: ... â™
+ out_fact3: ... â™
+
+ // The player goes on collecting more facts. â™
+ fact4: ... â™
+ fact5: ... â™
+
+ // The player again formulates a scroll, now being able to combine facts they measured themselves
+ and facts they previously obtained via scroll application. â™
+ view scroll_view_2 : ?OppositeLen/Problem -> ?SituationSpace/situation_theory_2 =
+ factslot1 = out_fact1 â™
+ factslot2 = fact4 â™
+ factslot3 = out_fact3 â™
+ âš
+ âš
+
+ theory SituationSpace/situation_theory_3 =
+ include ?SituationSpace/situation_theory_2 â™
+ out_fact4: ... â™
+
+ // and so on and so forth â™
+ âš
+âš
+```
\ No newline at end of file
diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt
index 4258dc0..13d12a9 100644
--- a/source/IntegrationTests/SituationTheory.mmt
+++ b/source/IntegrationTests/SituationTheory.mmt
@@ -1,10 +1,11 @@
-namespace http://mathhub.info/FrameIT/frameworld/integrationtests âš
+namespace http://mathhub.info/FrameIT/frameworld/integrationtests/space_typechecking_test âš
-import frameworld http://mathhub.info/FrameIT/frameworld âš
+rule scala://parser.api.mmt.kwarc.info?MMTURILexer âš
+import frameworld http://mathhub.info/FrameIT/frameworld âš
fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta âš
-theory SampleSituationSpace =
+theory SituationSpace =
theory Root =
// planar triangle in R^2 â™
include ☞frameworld:?OppositeLen â™
@@ -34,52 +35,50 @@ theory SampleSituationSpace =
meta frameworld:?MetaAnnotations?label "ð”¹â„‚"
â™
- angleABC
+ angleB
: Σ β:â„. ⊦ ( ∠A,B,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
meta frameworld:?MetaAnnotations?label "∠ð”¸ð”¹â„‚"
â™
- angleBAC
+ angleA
: Σ β:â„. ⊦ ( ∠B,A,C ) ≠β â˜
= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ â˜
meta frameworld:?MetaAnnotations?label "∠ℬð”¸â„‚"
â™
- rightAngledC
+ rightAngleC
: ⊦ ( ∠B,C,A ) ≠90.0 â˜
= sketch "calculated by ComFreek by hand, hopefully correct" â˜
meta frameworld:?MetaAnnotations?label "∟ℂ"
â™
- âš
-âš
-theory MyScroll =
- theory Problem = a: type â™âš
- theory Solution =
- include ?MyScroll/Problem â™
- c: type ☠= aâ™
- âš
-âš
-
-theory SituationSpace =
- theory RootSituationTheory =
- include ?MyScroll â™
- b: type â™
- p : point ☠= ⟨0.0, 0.0, 0.0⟩ â™
-
- view v : ?MyScroll/Problem -> ?SituationSpace/RootSituationTheory =
- a = b â™
+ view first_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Root =
+ A = A â™
+ B = B â™
+ C = C â™
+ distanceBC = distanceBC â™
+ angleB = angleB â™
+ rightAngleC = rightAngleC â™
+ âš
âš
- âš
- theory PushedOutSituationTheory =
- include ?SituationSpace/RootSituationTheory â™
- c: type â™
- q = p â™
+ theory Derived1 =
+ include ?SituationSpace/Root â™
+ deducedLineCA : Σ x:â„ . ⊦ (d- C A) ≠x ☠= ⟨(tan (Ï€l angleB)) â‹… (Ï€l distanceBC), sketch "OppositeLen Scroll"⟩ â™
- view w : ?MyScroll/Problem -> ?SituationSpace/PushedOutSituationTheory =
- a = c â™
+ view first_pushout_view : frameworld:?OppositeLen/Solution -> ?SituationSpace/Derived1 =
+ include ?SituationSpace/Root/first_view â™
+ deducedLineCA = deducedLineCA â™
+ âš
+ view second_view : frameworld:?OppositeLen/Problem -> ?SituationSpace/Derived1 =
+ A = A â™
+ B = B â™
+ C = C â™
+ distanceBC = distanceBC â™
+ angleB = angleB â™
+ rightAngleC = rightAngleC â™
+ âš
âš
- âš
-âš
\ No newline at end of file
+âš
+
diff --git a/source/Scrolls/README.md b/source/Scrolls/README.md
index df4a964..6c646c9 100644
--- a/source/Scrolls/README.md
+++ b/source/Scrolls/README.md
@@ -9,58 +9,58 @@ Let us write a scroll "Midpoint" that requires two points `P` and `Q` as input,
```mmt
theory Midpoint =
- // A scroll is a theory with two special meta datums referencing a problem and a solution theory: â™
- meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
- meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™
+ // A scroll is a theory with two special meta datums referencing a problem and a solution theory: â™
+ meta ?MetaAnnotations?problemTheory ?Midpoint/Problem â™
+ meta ?MetaAnnotations?solutionTheory ?Midpoint/Solution â™
- // You can specify those theories as nested theories of the scroll theory as such, but this is not required at all; it is just convention. â™
+ // You can specify those theories as nested theories of the scroll theory as such, but this is not required at all; it is just convention. â™
- theory Problem =
- // Declare all required fact inputs here.
+ theory Problem =
+ // Declare all required fact inputs here.
- For every fact, you may (but are not required to) give some meta information
- like a label and description. â™
+ For every fact, you may (but are not required to) give some meta information
+ like a label and description. â™
- P
- : point â˜
- meta ?MetaAnnotations?label "P" â˜
- meta ?MetaAnnotations?description "Some arbitrary input point"
- â™
+ P
+ : point â˜
+ meta ?MetaAnnotations?label "P" â˜
+ meta ?MetaAnnotations?description "Some arbitrary input point"
+ â™
- Q
- : point â˜
- meta ?MetaAnnotations?label "Q" â˜
- meta ?MetaAnnotations?description "Some other arbitrary input point"
- â™
- âš
+ Q
+ : point â˜
+ meta ?MetaAnnotations?label "Q" â˜
+ meta ?MetaAnnotations?description "Some other arbitrary input point"
+ â™
+ âš
- theory Solution =
- // A solution theory always starts with including the problem theory: â™
- include ?Midpoint/Problem â™
+ theory Solution =
+ // A solution theory always starts with including the problem theory: â™
+ include ?Midpoint/Problem â™
- // Next, we can supply a label and a description to be used for the overall scroll:â™
- meta ?MetaAnnotations?label "MidPoint" â™
- meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." â™
+ // Next, we can supply a label and a description to be used for the overall scroll:â™
+ meta ?MetaAnnotations?label "MidPoint" â™
+ meta ?MetaAnnotations?description s"Our MidPoint scroll that given two points ${lverb P} and ${lverb Q} computes the midpoint of the line ${lverb P Q}." â™
- // Here, the description uses MMT's interpolation feature by prefixing the double quotes with an "s".
- This allows embedding arbitrary MMT terms within the string via ${...} where ... is an MMT term.
+ // Here, the description uses MMT's interpolation feature by prefixing the double quotes with an "s".
+ This allows embedding arbitrary MMT terms within the string via ${...} where ... is an MMT term.
- In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
-
- If the user fills the first P fact slot by a point with label A, then the scroll description should also talk about A, not P.
- For that we can use the MMT term `lverb P` that stands for "label verbalization" of P embedded into the description string via "${lverb P}".
- Whenever the user reassigns the fact slot for P, the label verbalization will kick in again and adjust the result of "${lverb P}" to the label of the actually assigned fact.
-
- And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere concatenation (without whitespace). â™
+ In FrameIT, we use such string interpolation to give the scroll a more dynamic flavor:
+
+ If the user fills the first P fact slot by a point with label A, then the scroll description should also talk about A, not P.
+ For that we can use the MMT term `lverb P` that stands for "label verbalization" of P embedded into the description string via "${lverb P}".
+ Whenever the user reassigns the fact slot for P, the label verbalization will kick in again and adjust the result of "${lverb P}" to the label of the actually assigned fact.
+
+ And "${lverb P Q}" is syntactic sugar for "${lverb P}${lverb Q}", i.e., the mere concatenation (without whitespace). â™
- // Next, solution theories declare all facts that are acquired upon successful application: â™
+ // Next, solution theories declare all facts that are acquired upon successful application: â™
- midpoint
- : point â˜
- = ⟨0.5 â‹… (P _x + Q _x), 0.5 â‹… (P _y + Q _y), 0.5 â‹… (P _z + Q _z)⟩ â˜
- meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" â˜
- meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
- â™
- âš
+ midpoint
+ : point â˜
+ = ⟨0.5 â‹… (P _x + Q _x), 0.5 â‹… (P _y + Q _y), 0.5 â‹… (P _z + Q _z)⟩ â˜
+ meta ?MetaAnnotations?label s"Mid[${lverb P Q}]" â˜
+ meta ?MetaAnnotations?description s"The midpoint between points ${lverb P} and ${lverb Q}."
+ â™
+ âš
âš
```
--
GitLab