From 54d9b2b090196c90b2a54c7c8ea24287a8ec719b Mon Sep 17 00:00:00 2001 From: ComFreek <comfreek@outlook.com> Date: Fri, 23 Oct 2020 19:57:49 +0200 Subject: [PATCH] feat: label interpolation in the going --- .../FrameIT/frameworld/$Angle$Sum.omdoc.xz | Bin 1636 -> 1628 bytes .../frameworld/$Frameworld$Meta.omdoc.xz | Bin 472 -> 648 bytes .../frameworld/$Meta$Annotations.omdoc.xz | Bin 444 -> 720 bytes .../FrameIT/frameworld/$Opposite$Len.omdoc.xz | Bin 1608 -> 2068 bytes .../FrameIT/frameworld/$Pythagoras.omdoc.xz | Bin 1876 -> 1900 bytes ...$Triangle$Scroll_$General$Problem.omdoc.xz | Bin 544 -> 760 bytes ...ngle$Scroll_$Right$Angled$Problem.omdoc.xz | Bin 748 -> 788 bytes .../$Sample$Situation$Theory.omdoc.xz | Bin 1408 -> 1368 bytes errors/mmt-omdoc/MetaTheories.mmt.err | 2 - .../mmt-omdoc/Scrolls/TriangleScrolls.mmt.err | 241 ------------------ .../IntegrationTests/SituationTheory.omdoc | 2 +- narration/MetaTheories.omdoc | 2 +- narration/Scrolls/TriangleScrolls.omdoc | 6 +- relational/Scrolls/TriangleScrolls.rel | 1 - .../FrameIT/frameworld/$Angle$Sum.rel | 2 +- .../FrameIT/frameworld/$Meta$Annotations.rel | 3 + .../FrameIT/frameworld/$Opposite$Len.rel | 2 +- .../FrameIT/frameworld/$Pythagoras.rel | 25 ++ .../$Sample$Situation$Theory.rel | 6 +- source/IntegrationTests/SituationTheory.mmt | 12 +- source/MetaTheories.mmt | 4 + source/Scrolls/TriangleScrolls.mmt | 15 +- 22 files changed, 56 insertions(+), 267 deletions(-) diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.omdoc.xz index 373c9a260b4e9b0792b8ea06a8ea2762f93aa153..71042ec64dcd2d628c4fbfd128844e392f662811 100644 GIT binary patch delta 1476 zcmV;#1v~oW4BQNm83b3T1{{$cm45^<-k!<7bAe&}xc3>6HXZSpwnPuMq~0mqg>S=u zfxq#oO^;8(mJ#GK-u<HgYboBO)Wd<tHwS1apimHRGhShAZ8+$L*9YC#3|B(w*ri@6 zRgr5>euN^|vB@_Bcu&m-nBSIm7B<Eh57$9`)bns2U~HTGv5B(9G=m$Gn}17`1Do|- z8XD#(I9bqL?<~5;Fzm~SSbEJodj2I6QA(d$rKPr0QJU5~@DT3Qe7C4=^I^vD`HR;G zi`&|$12MlY0zhDpPxNt>szsHbl<Bg~B|!MyxBMehTtE2t%-PUmR31ii%lhPSdSk_? zt7U35YtVw;{&NddK2|cW)_+e3p68BHETk3?#LL^C`3t=ePM&skRN{P1Y`0y<v9<M> z1^PeLT!d${qK>)K3@)s?d!*+36Xh#aD}lq8SQgA-v-&K&IfJ1SB*7F91Pk)83h5#{ zrxur}W#JNwV1-Yzbr*^$t-X~d-t7q4_vn?~ne>M_$b^a#W5+ldn}6tD6#`!lK~q6? zO~|jOw`)Ire=NCD5lf)03Bd>*X*tvsTDPPpnykW+(=qCVQE?q;qn|OO1b1%+wk@w4 z0W{j_0|h}AT1Gh#e_j2q9aB7+9nSI7LSjx+Z|o>n+-{O%lW0-Ug?WgAc{T6f+)@EK zZe{@-sqI4H_skloOMlea?;Iu2BqeqQ<fy@u_rh;_m!*M;lg8F>5?)5JcI#TsghdS6 zUEWl#zkdL9|9he&gBUy&t&1G3vvU*d8BTn(aB<UMVs1m)gXY%DS6XT+`PhD_LKlwW zH5p7Va4wBdJCV1;+?5dASge2wb5b4vlt3AZBOrD7uL!sZw157kNI{hp<U2)d!{~Uq z;xe*mEyfi)j*{X(j=%$U%o;|^dR{|FrM;#PTsGw}koQXex^o$?Tni`tJ`DPJ_wQX| zOs#2G`7YAQL&g6K8ZFk(OY&`Y%bTg9$^GyA!}TI=nI$G{8m4hk02J`+F22HvGVW{P z`pE(Qby}hj$$zj&wGH=Q3vD#500a0D@!d>#eSJj-|H$iZ^;+;O14pGW!skjSfg-J= zly#%0IeUq`4iM9nN^=);Seh{?S=EC7*PT)eh}Ogp|5?H!)bX;!{hdm3AdU~ZRg40P z{k3>z9kbooaVJuST1a7R019fCnA_I}ZinQM@ok7}`hV~&2T(x6%9tWu#_inz6-&di zc?;X@t&1-|$SFbAHC!(I{$Og}H$lFRvs$?bZ}ox$pKyn^4*3Q?OeSk4BvJRzO2i;0 z=LHhs@p$3zjs5h|z$0{{PY@%!7x7gn&#^{PDxe?;@{2pn+f$RH6rmGx({8?vmoR>0 z3XGFT(|=O`^-E__06inHI9VP7GYk^JjCkxY=Tj5tlfn3+*$!Z{8qaxfsrg61)leJm z31`1*mvqx_9XWyW1?}PGwW>X+6#e>97#mC^G=OzZ`4Lwjy`^9xkm^lLM`Gh6+!B=k zQ7kK2hE!oYpfj}Yz?%VaX*^;j>i`K9TrK<G34e0?x6UD5z*?_DT&sjegN;qF*c!hz zFEB+S7b}@)90`+ThUCL_t*0|7Be6wQEWt5*RK)ZCm3agEQqcqF9!x{3NCGFi)2BRY zKjBZ8<VGm2;`?Y@%><fpqOPKBk3BdSBoJMJh10|@g4-g<Lob+gI()eI!GM5&A}Y^a zZhud0F@OM1@DfSx(a}ICu49^paffJ1Uk|3~F8Sh~?R9)|pEvmzVw>;J*gcMAPB#}l z=B6n(P5UGRp3&0V%0_;@oyRi8gXyU6k14~e%eBHbZFrN}5U^mg<ZH-t;!iQ;^`y!B zcs2E(m5T5Na*8%iDSCK$;W@7ixk`dpku|q2id?C7J)V??jNCV8goKO5v;Y8@Z$1Y5 e$y^Tr0k{mQuK@s8)nE&;#Ao{g000001X)@wbI*<d delta 1484 zcmV;-1vC2G4CD-u83a-y1|yLjm45^C<m;0|k%d@VA9tNb<9h<uOR@U~_C;Lac&2$G zcfzSe3#=E^fKc8~#yq`KoVqJ<U#Fq8!cKeQ>;2e1O}fiwCl5BD6$Ug-1(v5bop!Bk z*y<x`n~Uis4>uI4BK7dD>i8o!ev%zPIAw3Z`WZcECHtONQkQ*Do_|Ne5r1_<KT{qO zkLfx^yq<t-ozFY~us8)^Fcy5d^V!Ed=x|fWawY2EaqBIe!2HvJ!P22u(43SW7bB66 z3yR|08x0UW?T(XwQ8weZOzYE+^=n9)bqauX&WuB@G{(F^u?`uFc_&0dzfocir%B1o zBhu7;JU1_u1Gxv@&E?%vd4KV2GiIJU?S-?eVR4Hb)YZ+F^%Lo3CDl}&T|a2AYwGo- zWUd@=7dLy&G-E_!xPsCwuhtOt2qxhzIgF#4rkxcVilZl(t5z10n14?p7Vw_r9cUq6 z+E8CcM9X3yV;4adN_;Xy1BeLPosHd=E>hU$x^gzB!8}$eY3htpS$`?<;}0~x#0F~{ zUClSRmF|)0UV%WD$L<Z@|4v7Kdb#!4t=8?sR+TQY@qM`_M4)X-2n@l0y}}e{dn1>J z+r<HZPApsDbfLNWDfdipL<b7t#yW<6dI{XRD*qPA)I+?_6M_6(bX4(=vHveVxE+6R zG%29dYlP{?*Dg39DStB+)?`%cpk5t|=Hbxr!dK4U`M?Bcu;t3Atvrso*q;Wh7n2Nc z+8z)htLg~beX8qVXyD|yrU@1FKaGD2z6dr~U{{f^ndpD5$;(~Ha~SyOGp3dx^UW#^ zyE2Jd(iCZHJZmDSqZ9uEUZEEmXsT|))VshZ(=M*loF3%E3V$g0e5)(jkXq$J!mM+C z2g`P&oUZC7g9$LD5h|Td5?O-*z^XIFtWbutfNLI(2X*&9$`sj-jTQgCzTFGBW~Bki znZIgMmaOVEFnK$I{Cf_y#Sw3<NbFDB=iFKmZ|nZ{40GM&#Lx?JCx5T{KCS5D#H?S? zr4IaR<{9~*Mt_^Zazv+b<Aqx#QW{2kx}#CI;=@7wy&PX3li*EPXpPiXUya0wt(*r4 zmZ6)>1sG4#9?B*Mtj=FsMub%J71=R){VAKB#(_UkCTKo1nA5)eDH=Rz=ur<8&F-Y4 zi{fRSa-cP$8?90ypISk8|GB=#Q3S-Z1tx-0AJ*sz!hcjf-V^*I=YA^okmuOD)wVQ3 zTa;OEqjrCrE}`hTFC?LrmTGt9OY9S;7GQJ(5DLJt_Vw~z1A_a6*Z7{dQ6PJMP(Qxj zao9_)NePPm=-mIrAYc+u$^<4Q97JC|_~U?)=F%787JWEVa3wsT_Ou!h;VY}1Li+A? zU@D90iGSN{5Qc5G3X#|WmD7gx_vn2GM3*NMk^NvnFnSFpqfrqn$Sg~ldV6iK2W0ot z0+kg<A!(C6a#?W}Y4{MYl`>VdG1aIQy`{agm|ZRp8kC<%Ecu4przAZVI+NbAaN6Sb zn#i(IhfIuFTGt&v!llWq^-96c$1-nG`dbBs&VT<o%!V^RQ6HX`;ztQEGJ7Qw)B@{a zDWP0CtAlsfLV*SOa-d%mqEgw7_yjnv0O(i^PV)r!r`@1gjilD+hmK&qxt~TOgN~`S zyub|1wuUaY16dKgs_R&s6Vu>#0Yab<3%?pWiOS@fF9ZWZ<jbvFO;s02SQ6qxC#omX zkAKh=Nn0#vGr`kQhHacpz_sZ){i=@IZe(M72HW=hr`5(It5TESsW+MFAH}`64aBYl zOZbz}`!%CUtUtl(R{OVn!cXR}n6pwuXCNcmAn9@D=wf}y9*arp2sjb(uQE=|f8u;x zBtG!xmgJ7>%PaK-h<KwFw3dZYfwHs$^*s;xmeCtHFm$%~ZT9lPkuJo!^x{Cv>8!(M m>;M4lB&bu4%e{>N0ly5RqyYeG>Wy`=#Ao{g000001X)^}mEYw6 diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Frameworld$Meta.omdoc.xz index c6dde2467378c5ff4a036bb06d56e27ede374ea1..afd90f697c89d845f7f3ccecbc0fcae9f7029389 100644 GIT binary patch delta 412 zcmV;N0b~By1BeBX83Yb(0!5J>;eUF$Xf`<a9)&<wYq2oL5~%*VMp~@RVTx!@-=Fk- z>^JPJOmGy>ONteH(cp&DgTTF}mg5(j*eNc@$#rzsPK@Cks+vp>(i|~PPALR65%68Y zFD=X)u_DG@rqW(QU%fb1MQ#1#?_;Z32S=Be59)&lSy^p&8Wq!#>PZmjGk@Za3v6X4 zYuXf|A>S(@N|&^Ue^j`)$Jmk;Iue^tRBUz%CUU@+I!{RJlk1FcJhp~2m&VRSN!Uv9 zX*rMOG`t@kVRIK&j~_2s*+tg9dZ5N&r#>=qfAt6rO=|l3WEQl3L+gkq<aEaQaS?_g zONZ9cs)JR%n?5HSeFm7ognwXop02OIgf{0NjXycajid1nri~DA&qbt1eN>RKL-dd& zrWo&36L-5fiFUjBvFK`5C6UuDYJJgbDGE02BBEs`jR$kD!5`)9OhN(e+st!NH&B%V zd8j#+qT_S3-;p^b?mT;HGxq=h005q6K#U1a?`{AA;RNm+001S{Q4Pqk#Ao{g00000 G1X)@lF};NV delta 234 zcmV<G02Tj;1=s_S83YFY0hN&*;eTrbmi4y{0+3?Jt&eyX%Ln0FX3^i=1`HVH{wFyV zZfJZ#M?R^81rUsRcfii{x?^aE%4{5e^v>CBrihG9(nU=XPbtgn!UyzgT0CQP`QMV| ze&o;$orIFwz}M^!TKZz=eT@VV{^ZBR1j{FN?;-T_h!2oc4J_XaE{ab^<6F9fi&tjo zd1vyc*Og(w_F@pt%2`Eu<iD~XvAZ?$X*RfWGJY`4WESB#sad~@;y6wz%i|x?vH$=8 k0MnU2xj+}G_y7U11OE*G0Dt?wgR#VC`vL#}000D8T5`m2ivR!s diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.omdoc.xz index ff8d073b773284c7c3fb28332444012bca6d6e92..70d82f162407d7e4972b797ab9c3dcb0d644453e 100644 GIT binary patch delta 455 zcmV;&0XY7=1JDJK83YLj0*;X#{(qhyCBy08Ie>CMe+&P6wp-aHVh@aaGX6LlT*fyg zPgcPfsFq~2vk&Ro_rUij*Xh!B`R!SSgG<T%`-HZpc~0yp3x_brxPmWj<@f29UimxK zyWF8DM=b&a6s9t|biR6CC}Io&$*i23O>M0@_)|AZOtr1~Y~H}{kLCs;G=KOms7_8! zJ+W$WtewG3s9THe73b-eA!D`cBEJBFyFh}rr0<Kvp^g22Ku4v5c*CVE8QBk9w!At5 z)c#?U3b#GF1#dlGw$l_xH2h-w5=aC|*u$voYa>O?N_2UO@CY)wf!ZP@6CnTzgM}a5 z%w&^X?1*cBZofGl{5w$k_kZ1JnZ+4)V;mJMmc^BdEHgCUn)N6p-Sa+O2dkNM@c6TR zXS%RIFQ|1fAo-6fgfjmc1HI=>mEafPiCG>#R;E9W-E4{i+qaB0LO_{_%$j3bBCmx{ z(Q{j@e~V^|B~9m1Va4UFP=M0;>X7<G39_uAgR^&_K9mU>7toFgd^oU8!8lxQ%xxzP x1cjwdJ(sQdqe=+?008QWeztzt2Lu2Css)G=008fReT1>ZXZr#G00004Sy~hh*v9|> delta 177 zcmV;i08anV1-t{083YBJ0eX=g{(qNtvI``lmG9oGK+9$LPVj>c#FATVT%0XDyr6WS z_I=@(H0za|WAdO?fm%Br&mHfol}TeITRp=!p<U;9ya1i4CyJ8rObK+jbqiC;edh2e zFN6*1i7sYcmdGxKPF40l%Syfg=r?xUZ{oV<(z7BOdQncmJC*0OtbewS03rYYjJ~?* f5vUO100EW*oC^Q|uIdT2vBYQl0ssI200dcD$njD> diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.omdoc.xz index 5fe56876ee69f53b81ecdc065f92dc74cdfa704e..a5a882abc1cfad4cc35f3263d5f9e48ee0e01964 100644 GIT binary patch delta 1916 zcmV-?2ZQ*?43rR%83dJd2h))qn1AWR=@{!XbvHD#^iv!YE>{c%XIgD`PV^|Ck-6D1 z$<K84*^AH&e2qaM6DY36SyNFaBr}j?KaB2<g>SJM7!*`-%aN5wp2H?G!35ka;jp<- z>UPV0?aMad)}Kq;{g&7&vN?k>mSj-7A>c=BB~c-`N}6vXQQ4f1#RtIC5Px)ZOogU# zT!evD6S^r&4++I92b(C-VZilE0I&Wb@6vM?=_x7DFoq_iq#=@4Htbh#f+V|<LKwnR z?Fqhs(%hhe#NQ;hZ84;U*m=JSI(ABpuwE>4*W=<O4u~KA`eZ{Dv~7e*6XIqZ!s~mu zMlU%<Eo)3|uH<3N`Hmjb^?ya{gh+SqnxuInvQ~#66;wsH=0k7m&9X?ra`8wF0CPNJ z#LVJT=fGL-occ;Ad#Vg3L2*`&c;j|nEcu|A{Wun!qFKz@aC;T?2nBqJzBh!DX|bXK z@WIDW`qKtaC)|1h?1W-G94t-E(Ho>E2EBJA>zK%SdBGpZpJ-<`Vt-K9n+n>h_e4cv zCG4o9C;xVM;m?OFU~fX?a?<ha0%`t}!f{PygUgQ$wYO12a=dYYu1UXKHAbCN$4s6U z+8=znZOaSCH<)}c!DSR&9B_@=>h(nkC^(E`j@*fydIR$(Gxs`vkqlVVRHI*-ZJ`a+ zF_4qUe4IRlz=f7ia(`#vqa69~s{K0mllgkbJR+xRTV|zQ=RIHEv10oUmX}tVrx>u2 zeM||vI?-Dfb)U#*u7pHxkg$JjWR9`cCWj;&kqF`S1eZ*vD$oV$X^yxVabXr%UCCTL zVoQN@Q_={Wx3%IW@E6{7A6Pi=JRRvR5voMo9MqT6BMK1>+kYq`l`X?GSn>YIL4(J_ zjRSxE%@OK)qMnRoVk|N}$TVo-SPO3%eKnDB%-7w8pqw(nt$TGT=oz+lw}-;6pu{65 z8B%X*y=~sM%5?deRC(IEvS6wB{hNltKqb$6vVF)RtfL{IA~Z^6u9pU61LulYb8I^M z=$fzcL&ezpynpp}AFtFv^fsYwG<3^B4?Y_h?>!G@OeU}RAz(K0HI0WhoA%u0WhB~y zS!nH9@Xq|d8Ud0cAJoMg<<h>+fBjTof|&KaPcaJlwNaW6ZAxyM%%a76CHQ8+)DxK3 zacC!QnZJ8t>GY);r3eTV{hY>LJV?{rlEJ8xD25(F4}ZWaH|kzbC*{ZTGZ6Ud(46_t zXHrk^Ge`nh7+i3Yz!`u~>8YT^^y4+dE^6wTe!NwSg)6exCT;Oa5|LDrq2{ZpCNJn0 zLAx%`OesatFIHqE%~Do~lCY9vqVPh+m0U&59|)NSBNtw-J7){lk6006YnDiPzXikc z3QJQPOMkH%xI%V<^JiSm18zYpdw1LQ%|a-iim0Hi6%3(G4*($j0&|Q(%t=nRVlp^U z+~TjYJN!e7JxwNsb&TAo5TMUo2ek1w#<3@9Cm7<cBEx5TXt6Y0`7A(eNx^HxV01~` zjYE}6Ug^YefWnQ6HXtVX^fwpd^lxvlJy7St6@Q_WHlG|@MgZ8UR3I=4J!xlk^4e=% zw~Ze?WakJnVxkT{<z{dDTWEp4SJio(9=C5adO|ZbDA3-kG8PMP&#<w(cgQu~a}j8{ zq?ym3Ab*2&fAw8R)e<1ZQ+zL4aeu&DJePe6%GNgW<=g?XbLC)EI61B=I3L1U5velu zQh)iJqb$i%XsT`7Z=8$p2wbH+7yND+h?(VSUw>+#YwgLbc>dV|<A<p<U)_VgBNH+b z1oukmF>Y@nHKrkhk`}pG4JmsG8*!F;0m^CAeoN5Ozaq9aqn9;Bze>K-blTPS0XF*O z!fM7<adM1gvf5D0#Y{KLOr0qMO)WJs*MG*^A<WOtPrMz7_;-Vw-m+2202U*G+G{)e z^Ok(@OkDob&?Vg*^E&%~c<jLEUGWayNp&--%FQ%W^6FIl6!bCxSDrVf(-<qE<;&jy zJ6Y6VGn#P2EXMSqO(5v}MS1b(!xYqDK-BsYJDwxRJMF|0)UR%o>AnkGvdLIJ&wmAI z8i7|d!`zaxMrBDM<YA^~Q$z>%USzTp2^6EkuhT<QWigUzyH)3(EwfBPdWsPI2=vxZ zvG#;22>G;6qQt2R#$Y$q%UPDpma1QjAeP;uEBQIJl+O7B<I4lkA&0=33k2meOy(J1 z3mclJ-uxH(8}R4%-re_}t&m5aAb-=9n#H&WW?5n$!4G%>1Z0P1eC!_BQguSB=@>hR z=OhQ>*jFjb*&|9-G<8UO#7_Gx{`|$Zk>009dl*>tt!9`}!VP^Kmd$p!_>byXTboP^ zbgFbPB0p8r;YYLQ2-L%ECMI`yfd2@eCCCbi-5l&gHQ5MLE!2Br2%xC!{B63ZJY8{T z_Esz0341M&<T$VK8*h35=r9AmZCD6-JGBJ0#@$;6Zy_c?;^smFY0GYGSoCPAsW78; z%dhs&#qO8zllWZJZi5!80001B9l4FYYxySt0q+m>ssaG|ws!Hc#Ao{g000001X)@^ C)vdGu delta 1453 zcmV;e1ycHy5XcOW83a#A1_+TIn1AAahI|oX)QyyW*M{2G+oAeW*)=6x%0$SGERJ<D zuQv_NQv)~k?fdWH(6SRvv4gTGfUi2r%^8`*hh)28E$aFmq(_ZCNXakY+r(9OtB?B* zYsOE1LHx05Y2~py?VJlABKAw$)=ov>X<b3omn!5r<32Q3HBsuXFY=HCV}E$oI-dUv z&Lr*X1;Dudv?7WGp<$94y;N128z%&Oh;3##__7Eul|~;1x*zW52N4WYl{D3Hh<x{# za8$kf6}C^{Jk|DyeBhF`(h)OV>2ZpUMD2AL_`o5NcXH`9Pa`oqzj64RCNmn%%u0s! zrG9?$Bx4g~ox=)!zNs82*?$!&Weq;3=TwF<u}{Z7umtu<nVn);IC~%$ONTN#@N|P? zs^rOzTw|ll5h>t+AP5>%`N_{FDaJV3*rrsfGct<80(DO;7MDmeN<j>h_)U_<ApjD6 zrr3BdjTYaO7~Z^<G<#(bqu&@kYY{|&I^ZatFE7JRE?K3!1$WKo@PD16(m0Rno6X;{ z!TMU*OOuG{4MqNM4DLO$3wmH#!(!A1LbI&$hkOp`II`vLF=rui=UUZNVUzO^aPDEv zkE6OBvjYk3=(VT6mE8ia!65!{%>Ig^*zD91IR$Bk(JWzSj^+k{T7MBedE2m&6H^eX zP<RWZ4`Gha!OXIoe1D-`u!eh2S4}(XG0RLH?*Yfggh#cqy|a>gMgX!_YfpvHN@K-2 zXCB!l)C(IOpkr|TXk{*`62i48hPhpDsD>D>gk&DR;b|W7@Jytx*u|>Pj_#kX(Q*xF z?LV2`l>HjzTcC~p<N4xIVT#%fMtn?cdDhlr>(;?{A9T5fM}OCQU`o;RwXqHHWj98Z zBC%lSBet*}ou%91GEb^;$Z(C|%pZnPmYyei5Hk1l+hz_97x2St2llcvW)}rf-GB0d zQRn)3!!R$e^ZSQkS7SOB{Z4L4V@cEjwb~M-uK=J3t9MW-c{M-H2HW}9$Ka_DIl23D z$IdmZ@}TuXXn(mmK;qqE8VEzV%umF9FmDg@rCS}J9-aO7Z8&9T!nWsNzA)0LZnPSX zk{&vf{<z2$wz-mb!be&FtZk!E91Z1|mSRU?nK?@({MR3L&uavXY7r@C@w-|(Opq;u zSFiU#ly?nFlfM$<IL>><;>E~RYs$6cHN2^o&;wm84u5tX%6DhEYR9z=t{o|09;``j zZDfkOH|!_|I@Xh(VV3ryopH8oI<u9bK})m|y^sF$;vU$mQ>pWdW=D5!9QHUybf*qX zAfR8wUN%QL!J^_+#+48kw$T#NWq5grAOFt^4DFWAhxbSi`XjvGfvn(U<{07{5(~IW zxb`r&O@Fj@`YSZN6~rDM+tFM2H;_QFs;i{~%otBrftTfOCR_q#@4g6*_mBm3^2zZJ zGF~2NIBTGF!q{%!_2{CN5f;Ul+<?a#a=b7+bE|J3O}-|b5_{kOlbWWobiJJV0+}`e zYJjp2RB*?CmIv6sXW)T54^dw^ZK9`bn&vkNlYbAuUBHl<NC5gR`x0imDwkyq%YAd$ z461hBUq$iEh-HwHG2lIGsCq`bmQV)(n912}bGaM4yNu(@Ul0wCF>fMyJ#%}X_}4Yl zgiNWHVo*aT089xkZm8c}+EW)?Up?m<;saz*Z}Ffq2RN#`E0Q8<+f?y$U+?}vExA)x zxqrLxwu<V_TL9CG7928fiU(isRa?X>3cP@8+42KZH?nSy=edV7q3A~`&jvIX?{los zwp+eBYp$`7q-<N##TarWv3Cb{75Yk$f9N=Ag2dBe;<0=)@}ll>fL?*bGHPbnv%O_r z`5Iv&n<N`vNAvr~RR@Kv@_MKvk+lHtHy+*noQ{X700E>7$({iK6L0%rvBYQl0ssI2 H00dcDVw%j8 diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Pythagoras.omdoc.xz index 1c29455b911de928123dd7f7b2448a7a48e23e69..220acb5aaf530ad737af2ef4d70c27cecbb7d427 100644 GIT binary patch delta 1748 zcmV;_1}pj04(tw)83dKQ2P%;rmwyc2@jE+q7a>D4HrCO1CCdc;V2L~c%tcu`Dr5%! zLyGUJ%d!Ok?6~rG!z2SrCC)ML-znNxaNl(ql}@U-2Lp_;iIG8|SP4cq5fc0?Bg(t3 z!m<MHlfp#?Oi$R(;R-RPuLxS_I1V}II2B?4>6naQelPvSWgV1lu^8qVVt;wxv;R@R zrBk5fS!ChPPLL$E5sNYf+3@(*YFr5|?5K4R6qlatF!WH!Wt#DtRRYSUnl%?mr++r$ zTv<Se&rR$Iw{=J&QX2O~LoYX3ka<yi4OIrF(_<23Q!IubUbjq;s+R#do2YrQr*PKo zJHeYydh&-rk=V1H5va@+hJSUt=)Jq}!xKPv1>#Nax~+}DzImKnvl9_T*fuo(DD;}K zNFCgxGQZz9#BM3-X6t|+8#3I@Latv{@hp<BjdZ6s0{=(s6EI+5hqyoz3;OSiGv`(3 z?W#I--bM{Pz8m(eGRBk&brexgWDR>junN4TFzn`rS^Tk(dWoLuU4Mzvp#ihdsq0oX z>tl0VEsff7?p*SvB8e~og1gA3X{iOgDAgkxyYOIQhEO5AvAA@O+|1pM^<%OAa~kVb zDiyCH$p#KAtz}mZDKJG-bdeq6CPiJjyVk7@z|eY{5Ib6-U^{yDN(op_5R#cqpGQfF zOd_AEbjx};3_uceMt_@--xYKZk%*>F{wNJfJRXu79)5xFlvlYYvms9tLv=2bsoH&v zgsW`1to?Y?a0~c*x2Bv-uUa_D-TN<>kS9yvd$g1{h+3WPH`!ZlTaio36V}J}rGoji zVF`qah!^Wrn@Adnm}dZaA5b3hh*!Mmf4$yxaNDqm9+>zi3x7OZJgA}P+G1Q(X#Jma z{bc}#OQ8M|wPSD(wRmjtFuO)>M-Pw1^L51$wU-0@PlAisvme9<1V!`c>+b^q@KAZ5 z;D8AWE68fUmyht|O-O;i_3H|0Af|?CT^)-vmqAwQLzQC(-F1QNQ0*C3jOmwgUmkf9 zecAxxM8hXz*nePgvS}7V_o})(xDjk5s6Kvm0}rtTP^(=qpSeORovA=t0J@xqti`?; z*RvkMgfKk2Eq}B@f(dEzPc5d9OX%D^k0-W2%ZmX{PV9~#CD|B=mt_yp)|YVAX_6qa zlS>Fx>eIZ>0zMaC7~o1u&F~ve5DZDq?m^(&dpR5}rGFhI!@TX44$nCgPYR58Siuce zQkV?sZp%X}M!4?BO1?d!QhnMzCy|1=oU4korG}hY4AY7yYJMgESNN<{*?tEIx$xM) z`A?<?D0LhTcC|jr6>_Z`OYhAWGY!KML&CXLp<p!atH~_9ZZF(ei;`0QD^^R89PcuN z59&!<jDG`pUT;j~;5z?04#q45k^PJek(@&luq*`XEw7=C+_sjJ%H&s1!D$7Zb-Ou2 z>$3B-l0K?xhQ1ts4^@xaXZcx27Pzg+N_Bu$&py(^i}Z~Yic0|Gd61awTKsGq&4$l% zFq=||C%FdiE#p>r7Ny)K3*|)fX!*|M{E>7Pr+?U^VV(IY5Q8C07q1ht4)l}OlB_ii zS7h#iPN))_-AAhi2_LOkWY)&l-=~W2lY2IB{z<vEqPmRX_&BqORC%x~wkEO@&d|Gk zDupOcx`T8Kxyx<sU_HPW?f6Y(#wSfcL)ht@elZ=jtBWy0(TQu8Pvg{m_DhGSgVfEk z8h;v%FY)0%_spQWsfo=c<_8IMq$A-^waef_c)!)l9Xn&wRd90{-z;G0{ovUOo2IDp zqJ=~W&~k1)$Gx>LV8jgiehtYszj)pcI)#gtjKU4wuHz}4AkhI_Q*=g}+1{)@Kpj8c z1lR9|mJ@|n99Gez+#Z9g*B$q68KSQ-$A8BK^x7i3{GA>VvIT#CI;8SFNW6sfl%W%M zxg`5tbgy`2?C2I-R6+lt%<~7fe(<haqH6QWA=`MSf_F56ym*kz;5|EMI9lvqR$WX2 zT%*aIb1&}O69lx$&@1~L_8exZmAR8AV`xPD)HH9xy!WM7hs8d7HNRJV;RT-{HGj=@ zRp+AQ4~t6P?q0pp`T8O9y&|Wl+a!_Q{Ywk0pvF@(=f{-{fn>D>a0x$r)Wkc&V$8dv zdw}lLjXvA2kE7l}E3zc|E)l=vB`iWP1M?SmJLLy8ytCh&g&y}Lpv5Xk<I;d-WG<^1 zR5bTavQoyNvs!X7>>nii`Yr>TGDY;zDgUG+ZSMpW-#+a7=Oa{hW$1#I?3n$lu7KTg qTAyS90001V|8Wd(=DDN*0mcr!s{#N~(bu!F#Ao{g000001X)_jTw9U= delta 1724 zcmV;t21EJm4%7~i83d3t2NaPVmwyVc7jB7R>1`!07Gd5R$or(qyjutQ<HhLV6DZ~F zDCb5<6UOVTHD2@V-${Uslvf5qWZS!kb1=M4WrmCHcV14uD9eP~1iyF3TIpl!<S8$n zpG$hj_jZI!3d=@i%ch8e!S#TDJjE!a8v<qpn(r+SiQ29(xA8}@$M1>73x9b`!jl7h z5m2g<b%@(*^QxOB0mL${E9?<XaBd}S+f;mjk>2&QKUl+Hep9B<npO?_*)qzjHg2G2 zgmC=MB;!oy(+M6o(`y6dQB3|32v^g(&IMQFtR5h}Q0;)?&8-x;fms?xgxTfH6Zn<E zbQjTcL9AONaQp0mJ=nW+qJIcI<Cf3m=SPFzo8yD2plxt<@j2loUgaOKKq`E`X!e$q z&ZE%4iGfh2NB(kxZNm%kIz`!`^Q$Y&=J_lifc*I}xI8Ey+taU~&9rV5v;&$N4p30w zqd>-kpK3=?cQT0*kWV4p=(tJ{l(?u^ahoIYWvKtq7(X@sj|HZqA%8TZ^OLDo*N=gd z?ep10r3sDoUO{G{>*sEKj6%<M&jYBLD66)OFV~q5uoOgx%6+(b_&N8{sEhiN%Sl-> zEOJobC29?grbc^x7QtJS-}uKLCezvMgj?20;V|pitdK8^ZtUmIJT=mGE7q9xoOjBd z<Uj;fkv7O?e|Ojk?ti-b!}VL<sh$?a)ASstKYpD8vbv^G9Lveh<#>Zmb1r7wWCPw- z-mmUx48^V2wh@!vD>Jp%(6zzv=m}R56KG0dE$_?%^YtL$V1&lOoDOG>W3)aey}j|< z;9!m(8b{`w75X&l=XhayA2f5MC|?~cpxb{@J9cvoH?rGN!+(xt)e{|H{P~1wSbW_* z%#~d)h{-OjW#kC!QTK_x^PMG4h>y@m%oKk<v97T5S!Y<Ktf0X!NfQOc^zX(rRwbwK z%5%V8(`}?Yz31r@GC0pYl=Yq-VcMh~(1S#L;oOb>EM1-QTa;F~N-~H}?rlLg)uh~b z2%!Ur#Kuc?#((P(B6topUZcdB3|v)U%oW<C0fG}9HA08c7Y5@VdmKT^w+4{2tE1DG z=KHWg4<QW$+r<88|3POf9!XnQL0;dbzdnkylPXS%zX7@X068_@Kjp50Qcq%ZNmXk6 ziIlBJsDzolgue*4%gfb(^;DDHu!3jQ_fY&~=BKwegMUeQH=8`%V_<5mD|t`T<)X{v zHFSGhN;>~2ip>;CRPx3h$%<uD)IK`dXfPTi9?HL>*zZ3X*<$=^M{{PKa5aRL0MEYz zeryZ7ztYJu!nq~ZQ;f^!!_I{JF8qv*{-5P~gcUTlqXwSX(lWs5k9-Dh*0TpABjj-s zud|y~$$#pwy;9wgd`gbG!(_EnUX(G4(YG<iXWC!Dul`tzaqT}R-6d8OOdJ9c^ju^W z!|Yt6KVLZiGsjer<iU2z|0F~>p1^BIe8PicQ7;2U5e1ux!uueSOGt{&%FExFoRP!Q zP#i%DoUJKl;r!IdLRTba0Yyt!n+sBZEYe!Va(}2jFG0xYxt0w#ExDPA+O@AU$54nX z1mMeJ7-%EHUTg#QYj%!*!6AoxFoW{Rg0U@u*}V#?QUunmVtL3jn2rxlM?|OUfMh=S zU^Oq4;yx4snvyH9qS7B{260aEVU0P=;9I*1C|M%ZTBoNB0XrCrW11ok+!8tnF=FMc zXMaFZd$CNdiZWJn6*58~f>kmBlQl?4sC<3Cf?YB*kthotXSfD;=a+V^U2;igU}HiF z$wfCJb5qmfvU09b-GnL5&1bCn#VzfEJx=0;Oxjujec{>l>>&-lc&p@x?};#^sVve> zg=h<YRGalb0aci|i*qiylnws%5$}WECx4<n=mJ~|aB+PKO%69t3;DdQli8s;04EZS z-$cpv{9R(A;TqySl*R^X3-oKRWWwprUp<WKg_@7@U5!B5_jDGc@!DoWU`!_qVa6{c zz3h)eUR??vn#pfwP<{dYcFkh-{X?d}a|tKo4_I)^<EW|dW-X`A?nRA!*p1+tr++Nb zAJy-;FC{um93QX)(dr?;L#s7yhY$Yp5(+d7^KY%$l9D|{H@`wFZ>#tyC@CpKnkdx! z+FKWp0I1SkE-yU8=^1A2rMS+2uM6~1XsYbWWOQotP>Ez9q&60vt-`gHSFwVBL%kE_ z-Km5n4*L=AgNcj2miIaSDt|Xwoh`h_K1fTTDi{2u*|7j6qYjT*zp$ME0k96WpaKAc S_)Vv=#Ao{g000001X)_q$Y3h~ diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$General$Problem.omdoc.xz index 4ec13830ea8b25ebcfd3c77e538a5ba3d4f96248..c2c96a06e1e46ffb8de29265790a98cc012b8752 100644 GIT binary patch delta 538 zcmV+#0_FXn1o#Dz83Y&90=AJI)PGl{y=xJd{PH{*OAw2~SQ1ko<LogDPq*t1?jw_5 zQZxzE#=<-1=mPQgmJ)!$FUM#FNP>6Sl1@2uqj}Zt0juLommg8qVC@hM>8B&ZphcsK zfYYu#$Q4`hWXNp-a0jqxU~w&H2jaVJjv$t9XQH9)EsmWHth|!3-0BE5>wgvj`3tqk zifl?NJe%?#B*Gc)1Ld?H$l}b@oi@>Lv*22|91Dp4BPts8P*RRaR_~Y3TZue~QM&)C zT}IFhO)FlNN%;QKsZY&Hg1$dIlUEsI)90Qecj_(w!DXJ>oq@FUfT-#9UcgcgA=(B% z3<T8lXm|k`xd%tOl>t?1<bUEDTg|)^dm^G)DTqtpVEItIj?U!nM2re(iln*66m!<( zb;qTO#U&8Dmy;^OQP(36UuJlNl#wkfy9ztS2pPNZA4>hOChj&K2uEKMP&{XDSkbNA z&|-q&eTy(egrun>ImfVE*nR2Fv%U2p{pMg}-0du;Xm|NS4tRn$KY!wp^_i;xrfF%u zGRC+(!*19J^bqv2?$yU%Ypl(dQDNG<#nk7op894HrNGFoIc!$?#7Bo!f04__YYQ@W z?Xed^-VwVVskQo(4d5w8%pljmRtx>UDsDS%VVA<drR;#Qd9uwAdjJ3c0OPU<2TD=0 c00Ghk)h_@5|E}0}u?xg!`vL#}000D8TKW75P5=M^ delta 320 zcmV-G0l)tE1)v0w83YQb0p5`v)PHT<(*iFc$Q2z{iR%@4aRrIf62!f9gmagqLf!UZ zR*B}$7kVe0dL7gDJfa;u`P?)B$4>`R#wJQ38iBs>;L=QpR$}HLiPG88eB;m)==+Qu zSqwF?sP%TradZ~1K=w=VQ(9M<eN2u@V+W$QypVX|OU80c+QK!XB7cmbD}TaaH*Gqv z@qU$c)ZugQ^)^XNB*5LmYO>QzL#%7nRIOdo(u76#8bBrIn&!gRcwWq%ICv?c?1j81 z>8k+F+cquzN+_;T!wI&TReETHwH7X1Ym%T}6Rme{9zqfwohuR8vMN!kLd+Byh9Caj zP@ayIS^#AQS8dwOzV#+}>M?C`c=d(s3~B!*DJsGM0000i0oDDEAt^op0r~@}6#xKc SqjDOt#Ao{g000001X)_M8I@xI diff --git a/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/$Triangle$Scroll_$Right$Angled$Problem.omdoc.xz index 1ff184df7047ab5d68a942b06e2b1cd91e7b30da..c549a1d9ed0db2f21638365c291c43d0c72b5187 100644 GIT binary patch delta 533 zcmV+w0_y$j1(XJm83Yd`0@INl^?yH27S50Cmog@uN{;5;${9R=CM&pj2nMOy_3zu? z+e8W^#BkkVsor*{E`<4Pd7w6L4!Nc^LC5M(NNrpZ=0I=SOvIn~*AL6AyG`fOBmC7g zLM0f_SZ$@T`<9C*zSB`C7>Cy&*b_a62;*|BNJVStZdc#37>A^Nuanvnh<~{Ea4b{g z(8nWa{*;xC&i`%2{8+_I*_&oT!A4?wB{#jr5#(0fVInD`S#<!m&t5b>q>^rH%jXo{ z>qEJ?;BXmo*wg344^tD<v|?}}NxqA7BUri$^6G71WMj|JQU%9&Sll`^yCG{{uExrs zTF)(>16#O<X}$_%wtvVsM1S}>v;U~!`Ae$}rxlBRN13HtlN@bcXA2iJLU5M`jm-;q z3Zn)l6RUb@`bGZZ<w)!>sCkX@3cV>_4go(O^P|<|FdlBSSP6emDZ8T+baCKMRiuxM zr4NA2$#km0eo=luqswP=dGT*w^swC!w{A#i+Z{pT47tXwE~ALoF@Mm=jGJstTPN9M z7y*n-cXBk=k}6KNuU16cs=e0h1RX)7ORDlZu;lMa9-@VgH~&2=zD=KM64<>0(|0O5 zvLwN@=afyPE3CRNOrfif#pWJRbY!>O;zeaM>F%OS`Ul0D!vFxWdAoUJlmo8-0q+H+ X9smHhm8yWT#Ao{g00sa600dcDF24ku delta 492 zcmV<I0Tcd|2J8ip83YYb0;`c7^?y8Niq4Phmog@L7<cQ`g(7@8oo32?U!4hdLq#vH zFfe@?Phmw0G(0}R)s>XELTsc=EQL(_D_yo=``8dK#A4*jm=$%eM@ZAicHd@BJE2d% zZp|bu9zIj$pu9Tn$Y{0}%`|GxsL%pM$x&qKBBRc1{ua1TX}kmqBtO-{D1YV6=~QHQ z@Qs_-_Yd)(kBgg3bV9C6W2SGlY{xcB0Qe3iKJubTC>a=%;20~k77ikoP}?{xnq$hW znp--ha)fKt=4#zQx-*aBl)L?Ad>#!wZjx6|%D<zK^^2FF05%m)0RMf1mf5n^@w$w* zjGAdq$BKgq>hZ|z5zRk9mVYub>ii6sKrx$S#MI6O{ExTCyKHEQMZ#6Q=R6q-YUKtJ zP3FT7In!r5j#J6r(aSd=QC9Hma0YDx@v@rZe?)Cz`)A!+<4%FR@%Ryh4VPpdm2pP& zk#*u4zYdyze<NyCKD33JIL+$LU>jC&Jh*8n<gf2(MC;MSP>>4SYh6yH#qUL%*;^S6 z!_SznV`R#f0=eGegrzE*Y@!RwdIcGg_sDZg#mJiQ%eE*StoR+hzv(MWP9(NE0001( i8EjW0h_j~v0mlW=8UO(MjRA<U#Ao{g000001X)_j=j|H+ diff --git a/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz b/content/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.omdoc.xz index 318f4e27bbde5a4ab5ed0a1fcabce6c18e630af5..b50e33a2fb6a16b5bd16f65b081f013d5312e3ab 100644 GIT binary patch delta 1141 zcmV-*1d98B3)l*f8Uu|56_Fj>fAiz{<(E7~UQ_8^rRF`@orzkEK4M<Djm!aJBL^`S z%hK(Ot%E`|@_}WMb295dAFu#pJ(zH)z%liB{6sePM#OoE_mVW!B7iHKKAytFD-2P; ze8+{l)OlDm{IB3*J;^FDjBXfLS`oN}l5UN0meUbJZqEjI24gTYhAUaPf4l?mki-w* z4$3b9Xe8e7RDhu4FZ1l=$1R^Kfa-h=dW7Oed$zV8@X+2<vYjHT27C29;z2+DhsFB@ zo#3^pyWb7Txk6|-57MF-<&4q6BYFI%P^WNT`~L0-HHS<+4a(Hq%H4|%hAD0sgJ!>h z_{{gtV&AEYMQj0hux;>)f8Jux7iG(#8E>ZD1JGLJhBk!)2piP#b-5GF&tDs4Zu!&h zQ@q|TY8UxNAB7tEk~^6{nteymLC;;&Zv@fwt^CWsa%>s&8Ibm;liPY^0q&cqQd6g$ zTv>Cwv{O&p^-FZT=(6~lE&r?yeeGPDm1-N?bZcw31li@|xSyL$e<zvku-~)`%QT10 zh))SFS~Q8P1K0KmM5U<@RV2P8)%OjYK{Gos+vz3lmG-n2D<yHAdyoV*lVBAMcB@{G zps@E4Nz~~MZW{&*rvbupFguQDL9<)#(h2i()BL?uv(YWjJQ=!RgM#h1?^9XG@RkTJ z>6dGG&U6(c%4%t1f4(dM+F&-VW`H->$&}T>?KfA=#xcqXwhV{6Z@337eV2&RKmKvV zrq7nL?i=?`Uv1$!TP0}Xi*gs{tu+{2x0TkFqn(>htn*I-Xq@UAb47N=yQigC?SEAu z>Xfxn<bl<~>=SO3Kcs3py<Fm?Z!<+l&CzW_6{iEtoz~HHf4hlhMx_lTvVv1dWfckr zu%b#Wr5~KqSp1ZBz`}=F@*UEB_xxt?nc*4ME&fz&>aa6>8b1)xd7f3ngPtSF=^&v) zQrtKYDoB05-36><1GlG<?zQGKw;9#2l;ydd7ZhYdnr<OJq|}MhD%SCdBy?K#BGpiw zR<Njo3YrLSe{@d}eB9q=0C0He8^GQ|IhFH8m5C(v@t!Xxue)^)SW|CguV%8;8a;|W z9>R({T3_9n)JbgNZ{0B|`JLcnGH--F>O-964lKhD%nxH}7Hz;<gY2sAuLD1*{V(90 zK*xZ8tP^~hf$<I{OciSDj`R#Zz6wub2+MUYIs5pxe^D)mY;wdA<V<~8xa%fMLy61< zdZ1>{i0`F_n}=x6*U^x;x2eE|LwF0twzxNfcmah<xWS2P!7S`bEqWW+8yhudZIAY4 zZK(^{lH#P{D(XqOY9j3FFi0}1d4d&$g0IIeY$!plpr@EX)~#5yK8YI~&Nt7U>eH0p zEIkpHXP<=U6e+-UG>6ue5GTSKnJs3SRK)Vj9OOK9*{X|+$JrxRGM-zWy#_U0Gkk0g z4HF+%48fR`jF-LW<FMx}o)%vK000001>y!;R1%8C00FTIj=KQ>6z%1OvBYQl0ssI2 H00dcD<Eb`X delta 1182 zcmV;P1Y!Hw3V;ic8UyVGJ&_&UfAmvk3cub4zcv^}t;N1|kGJ+`JO)(&pG2co-{UYM zB3~pl5%V;V?TvWUqn@Mg#vFepT*8z%ax4)oKt6}YV=PV>IZFcf;axqk<|AR)pVk2a z7Q+9Q9@zebRo?(OfXC~{c%WBq$r?g_*br%T=3Cos2m%R9zuWw-m+y-|f4$vXJJRx+ zh-ED(OLjx{JE&uP)QF-CBT3+~Fe+{sZ9QAEn;00HyBUn7P2K7Uo2CdI7Ye9m8*|mF zu=nV)Ld4qIbJhAZEr^m2|18xp<6LMAqG6Hui)7N3ewkd!G57PAbIe79o3Bb~B0v+* z=ZDHDd_>n@Na)MTWV&fQe>FLf(*D)eH;~Z3V%lGjZQs_0L8A=WL*lZ16slek<9qWJ zu;(PUUU@Tr2eh)eofVhVBHF|YHn1)`Mg<p2U(5?81yp;-gcqZ{lgDMr4q#Pgt|Gm_ zHegi-YTt2z?W@P9&YjKWlgb^g<pX4&XM-EdHU*J7(t@z%phJp}e{)!h81Kimfrd-9 zLW1^G-?BX7>Hj0#>ho0__5`UkaRUlsJ{p#@!Cr~rn@-_DNF)Zse<J+9d1$PRANpY| z%!WF4QIjj%22vwfqyQ`pQJ8~D+dK%sriy<au(g&xM%4i~^}I)5vxqnQ@AMmmBSw@` z=2YB^P^F+9e1qY(e*-wkMz5vlJi4Z^aLzo&7*Z;xr&m4H39-$)Vu!M|%jCf0p%=G& z2U!<9#LYr@-;##HWUX%RMHIL6Tn76;F_rlrd{XeKob>Py7+!?Z0E;+fHH;mu1o18R z;%B8J|FbfWzy)BW9UPf47WS-)ByexuR;o(}qpx=KEz##+f4*R@Ns2|nw6a(jgDIU? zSz?cR8}SP@zw``ouu-oMwX~tkrX!Q;hCoOJ6`?QvUN0(b9)YR#B;aIpgiVoWM%1;l zoSx;5yweDq#m@C?`6)t$F@+?J`BFknFKa*$W>}10V*dhUF`pF_u}L`h3!_|Y;XCQ# zR<ao<3NBv}f3YPISeADXisVxZ=M+NuDZ|I2dx_D96lN-Q?SocL7^-B_VTy@n!B!CT zmk}u%2I}_?wka%5%tT9clnQ71^*htC6_*GFfZ1+ai97p@y`p|dErUG<(N9aN@qOLu zDwB{Ze+$-!I{8v{l~MImzYhU&Hty<L4!PsAe=Q|jfBUxjC`WV_CQYk5LPD@Ok1Ft! zp3uwG>*+VRz=7PS)rBYUc=JP%QJdh|S)!PnXlgvUOw)_nwcCv8SEPXIuw8E1DyMX_ zI>uC<*#Fu;C_KQrH|l@9&3hfvu1TbNe<Ma&gU`?ifIwKn0eac>6r~8H_r$s-_zZR$ zFSNB0f6&gY)E)s4z9G&_&e|hwBY(_(o^>ES<*Ga42i0b9xjbi5W@oYcm?^JaKKE#3 zxf)*T4-v6Rgc#-`q~Gcg8x(@$&})eTeCgs=3ww})D7=hcA5iygno7~1b5fDw&Dx93 whx8pBU_Z|Q00000Dri+;l;e>300G$w?z;g15FnRiTCv1u`vL#}000D8TA}Sd_5c6? diff --git a/errors/mmt-omdoc/MetaTheories.mmt.err b/errors/mmt-omdoc/MetaTheories.mmt.err index a003a31..e69de29 100644 --- a/errors/mmt-omdoc/MetaTheories.mmt.err +++ b/errors/mmt-omdoc/MetaTheories.mmt.err @@ -1,2 +0,0 @@ -<errors> -</errors> diff --git a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err index b94e29a..e69de29 100644 --- a/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err +++ b/errors/mmt-omdoc/Scrolls/TriangleScrolls.mmt.err @@ -1,241 +0,0 @@ -<errors> -<error -type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition: Judgment |- ⟨,sketch "By Pythagora's theorem"⟩ : Σ x:â„.⊦d- A Bâ‰x" level="2"> - <stacktrace> - <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17(RuleBasedChecker.scala:99)</element> - <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$17$adapted(RuleBasedChecker.scala:98)</element> - <element>scala.collection.immutable.List.foreach(List.scala:392)</element> - <element>info.kwarc.mmt.api.checking.RuleBasedChecker.$anonfun$apply$15(RuleBasedChecker.scala:98)</element> - <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element> - <element>info.kwarc.mmt.api.checking.RuleBasedChecker.logGroup(RuleBasedChecker.scala:17)</element> - <element>info.kwarc.mmt.api.checking.RuleBasedChecker.apply(RuleBasedChecker.scala:95)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17(MMTStructureChecker.scala:314)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$17$adapted(MMTStructureChecker.scala:290)</element> - <element>scala.Option.foreach(Option.scala:407)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:290)</element> - <element>info.kwarc.mmt.api.checking.MMTStructureChecker.applyElementBegin(MMTStructureChecker.scala:73)</element> - <element>info.kwarc.mmt.api.checking.TwoStepInterpreter$$anon$1.onElement(Interpreter.scala:96)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.seCont(StructureParser.scala:131)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.addDeclaration$1(StructureParser.scala:501)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:692)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element> - <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element> - <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModuleAux(StructureParser.scala:587)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInModule(StructureParser.scala:481)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$readTheory$2(StructureParser.scala:772)</element> - <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element> - <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readTheory(StructureParser.scala:772)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.readInDocument(StructureParser.scala:420)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.$anonfun$apply$1(StructureParser.scala:93)</element> - <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup(Log.scala:34)</element> - <element>info.kwarc.mmt.api.frontend.Logger.logGroup$(Log.scala:31)</element> - <element>info.kwarc.mmt.api.parser.Parser.logGroup(Parser.scala:237)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:93)</element> - <element>info.kwarc.mmt.api.parser.KeywordBasedParser.apply(StructureParser.scala:83)</element> - <element>info.kwarc.mmt.api.checking.TwoStepInterpreter.apply(Interpreter.scala:102)</element> - <element>info.kwarc.mmt.api.checking.Interpreter.importDocument(Interpreter.scala:53)</element> - <element>info.kwarc.mmt.api.archives.Importer.buildFile(Index.scala:159)</element> - <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTask(BuildTarget.scala:564)</element> - <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.runBuildTaskIfNeeded(BuildTarget.scala:470)</element> - <element>info.kwarc.mmt.api.archives.TrivialBuildManager.$anonfun$addTasks$1(BuildQueue.scala:123)</element> - <element>scala.collection.immutable.List.foreach(List.scala:392)</element> - <element>info.kwarc.mmt.api.archives.TrivialBuildManager.addTasks(BuildQueue.scala:122)</element> - <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:389)</element> - <element>info.kwarc.mmt.api.archives.TraversingBuildTarget.build(BuildTarget.scala:383)</element> - <element>info.kwarc.mmt.api.archives.BuildTarget.apply(BuildTarget.scala:227)</element> - <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1(ArchiveAction.scala:119)</element> - <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.$anonfun$buildArchive$1$adapted(ArchiveAction.scala:96)</element> - <element>scala.collection.immutable.List.foreach(List.scala:392)</element> - <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive(ArchiveAction.scala:96)</element> - <element>info.kwarc.mmt.api.frontend.actions.ArchiveActionHandling.buildArchive$(ArchiveAction.scala:95)</element> - <element>info.kwarc.mmt.api.frontend.Controller.buildArchive(Controller.scala:74)</element> - <element>info.kwarc.mmt.api.frontend.actions.ArchiveBuild.apply(ArchiveAction.scala:13)</element> - <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle(ActionHandling.scala:48)</element> - <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handle$(ActionHandling.scala:37)</element> - <element>info.kwarc.mmt.api.frontend.Controller.handle(Controller.scala:74)</element> - <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine(ActionHandling.scala:33)</element> - <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.handleLine$(ActionHandling.scala:31)</element> - <element>info.kwarc.mmt.api.frontend.Controller.handleLine(Controller.scala:74)</element> - <element>info.kwarc.mmt.frameit.communication.server.ServerEndpoints$.$anonfun$listScrolls$1(ServerEndpoints.scala:134)</element> - <element>io.finch.internal.HighPriorityMapperConversions.$anonfun$mapperFromOutputValue$2(Mapper.scala:82)</element> - <element>io.finch.Endpoint.$anonfun$mapOutput$2(Endpoint.scala:102)</element> - <element>cats.ApplicativeError.catchNonFatal(ApplicativeError.scala:203)</element> - <element>cats.ApplicativeError.catchNonFatal$(ApplicativeError.scala:202)</element> - <element>cats.effect.IOLowPriorityInstances$IOEffect.catchNonFatal(IO.scala:767)</element> - <element>io.finch.Endpoint.$anonfun$mapOutput$1(Endpoint.scala:102)</element> - <element>io.finch.Output.traverseFlatten(Output.scala:57)</element> - <element>io.finch.Output.traverseFlatten$(Output.scala:55)</element> - <element>io.finch.Output$Payload.traverseFlatten(Output.scala:141)</element> - <element>io.finch.Endpoint$$anon$25.apply(Endpoint.scala:109)</element> - <element>io.finch.Endpoint$$anon$25.apply(Endpoint.scala:108)</element> - <element>cats.effect.internals.IORunLoop$.cats$effect$internals$IORunLoop$$loop(IORunLoop.scala:139)</element> - <element>cats.effect.internals.IORunLoop$.start(IORunLoop.scala:34)</element> - <element>cats.effect.IO.unsafeRunAsync(IO.scala:257)</element> - <element>cats.effect.IO.$anonfun$runAsync$1(IO.scala:177)</element> - <element>scala.runtime.java8.JFunction0$mcV$sp.apply(JFunction0$mcV$sp.java:23)</element> - <element>cats.effect.internals.IORunLoop$.step(IORunLoop.scala:185)</element> - <element>cats.effect.IO.unsafeRunTimed(IO.scala:320)</element> - <element>cats.effect.IO.unsafeRunSync(IO.scala:239)</element> - <element>cats.effect.SyncIO.unsafeRunSync(SyncIO.scala:48)</element> - <element>io.finch.ToService.apply(ToService.scala:33)</element> - <element>io.finch.ToService.apply(ToService.scala:12)</element> - <element>com.twitter.finagle.ServiceProxy.apply(ServiceProxy.scala:12)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.tracing.AnnotatingTracingFilter.apply(TraceInitializerFilter.scala:142)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.tracing.ServerDestTracingFilter.apply(DestinationTracing.scala:54)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.service.DeadlineFilter.apply(DeadlineFilter.scala:267)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.filter.ExceptionSourceFilter.apply(ExceptionSourceFilter.scala:50)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.filter.MkJvmFilter$$anon$1.apply(MkJvmFilter.scala:30)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.tracing.AnnotatingTracingFilter.apply(TraceInitializerFilter.scala:142)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.http.filter.HttpNackFilter.apply(HttpNackFilter.scala:156)</element> - <element>com.twitter.finagle.http.filter.HttpNackFilter.apply(HttpNackFilter.scala:113)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.http.filter.PayloadSizeFilter.apply(PayloadSizeFilter.scala:123)</element> - <element>com.twitter.finagle.http.filter.PayloadSizeFilter.apply(PayloadSizeFilter.scala:47)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.server.BackupRequest$$anon$1$$anon$2.apply(BackupRequest.scala:31)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.http.filter.ServerContextFilter.$anonfun$apply$1(ContextFilter.scala:15)</element> - <element>com.twitter.util.Local.let(Local.scala:4978)</element> - <element>com.twitter.finagle.context.MarshalledContext.letLocal(MarshalledContext.scala:157)</element> - <element>com.twitter.finagle.context.MarshalledContext.let(MarshalledContext.scala:104)</element> - <element>com.twitter.finagle.http.codec.context.HttpContext$.read(HttpContext.scala:114)</element> - <element>com.twitter.finagle.http.filter.ServerContextFilter.apply(ContextFilter.scala:15)</element> - <element>com.twitter.finagle.http.filter.ServerContextFilter.apply(ContextFilter.scala:12)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:13)</element> - <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$3(HttpServerTraceInitializer.scala:20)</element> - <element>com.twitter.finagle.http.TraceInfo$.$anonfun$letTraceIdFromRequestHeaders$1(TraceInfo.scala:105)</element> - <element>com.twitter.util.Local.let(Local.scala:4978)</element> - <element>com.twitter.finagle.context.MarshalledContext.letLocal(MarshalledContext.scala:157)</element> - <element>com.twitter.finagle.context.MarshalledContext.let(MarshalledContext.scala:90)</element> - <element>com.twitter.finagle.tracing.Trace$.letId(Trace.scala:104)</element> - <element>com.twitter.finagle.http.TraceInfo$.letTraceIdFromRequestHeaders(TraceInfo.scala:103)</element> - <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$2(HttpServerTraceInitializer.scala:20)</element> - <element>com.twitter.util.Local.let(Local.scala:4978)</element> - <element>com.twitter.finagle.context.LocalContext.letLocal(LocalContext.scala:51)</element> - <element>com.twitter.finagle.context.LocalContext.let(LocalContext.scala:24)</element> - <element>com.twitter.finagle.tracing.Trace$.letTracer(Trace.scala:124)</element> - <element>com.twitter.finagle.http.HttpServerTraceInitializer.$anonfun$make$1(HttpServerTraceInitializer.scala:20)</element> - <element>com.twitter.finagle.Filter$$anon$16.apply(Filter.scala:406)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.filter.MonitorFilter.apply(MonitorFilter.scala:66)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.http.filter.DtabFilter.apply(DtabFilter.scala:25)</element> - <element>com.twitter.finagle.http.filter.DtabFilter.apply(DtabFilter.scala:12)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.Service$$anon$1.apply(Service.scala:16)</element> - <element>com.twitter.finagle.http.codec.ResponseConformanceFilter$.apply(ResponseConformanceFilter.scala:23)</element> - <element>com.twitter.finagle.http.codec.ResponseConformanceFilter$.apply(ResponseConformanceFilter.scala:18)</element> - <element>com.twitter.finagle.Filter$$anon$1.apply(Filter.scala:93)</element> - <element>com.twitter.finagle.http.codec.HttpServerDispatcher.dispatch(HttpServerDispatcher.scala:42)</element> - <element>com.twitter.finagle.http.codec.HttpServerDispatcher.dispatch(HttpServerDispatcher.scala:23)</element> - <element>com.twitter.finagle.http.exp.GenStreamingSerialServerDispatcher.$anonfun$dispatchAndHandleFn$2(GenStreamingSerialServerDispatcher.scala:83)</element> - <element>com.twitter.util.Local.let(Local.scala:4978)</element> - <element>com.twitter.finagle.context.LocalContext.letLocal(LocalContext.scala:51)</element> - <element>com.twitter.finagle.context.LocalContext.let(LocalContext.scala:28)</element> - <element>com.twitter.finagle.http.exp.GenStreamingSerialServerDispatcher.$anonfun$dispatchAndHandleFn$1(GenStreamingSerialServerDispatcher.scala:83)</element> - <element>com.twitter.util.Future.$anonfun$flatMap$1(Future.scala:1812)</element> - <element>com.twitter.util.Promise$FutureTransformer.liftedTree1$1(Promise.scala:240)</element> - <element>com.twitter.util.Promise$FutureTransformer.k(Promise.scala:240)</element> - <element>com.twitter.util.Promise$Transformer.apply(Promise.scala:215)</element> - <element>com.twitter.util.Promise$WaitQueue.com$twitter$util$Promise$WaitQueue$$run(Promise.scala:91)</element> - <element>com.twitter.util.Promise$WaitQueue$$anon$1.run(Promise.scala:86)</element> - <element>com.twitter.concurrent.LocalScheduler$Activation.run(Scheduler.scala:167)</element> - <element>com.twitter.concurrent.LocalScheduler$Activation.submit(Scheduler.scala:126)</element> - <element>com.twitter.concurrent.LocalScheduler.submit(Scheduler.scala:243)</element> - <element>com.twitter.concurrent.Scheduler$.submit(Scheduler.scala:78)</element> - <element>com.twitter.util.Promise$WaitQueue.runInScheduler(Promise.scala:86)</element> - <element>com.twitter.util.Promise.updateIfEmpty(Promise.scala:783)</element> - <element>com.twitter.util.Promise.update(Promise.scala:755)</element> - <element>com.twitter.util.Promise.setValue(Promise.scala:731)</element> - <element>com.twitter.concurrent.AsyncQueue.offer(AsyncQueue.scala:123)</element> - <element>com.twitter.finagle.netty4.transport.ChannelTransport$$anon$2.channelRead(ChannelTransport.scala:169)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>com.twitter.finagle.netty4.http.handler.UnpoolHttpHandler$.channelRead(UnpoolHttpHandler.scala:32)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>com.twitter.finagle.netty4.http.handler.BadRequestHandler.channelRead(BadRequestHandler.scala:42)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>com.twitter.finagle.netty4.http.handler.HeaderValidatorHandler$.channelRead(HeaderValidatorHandler.scala:51)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>com.twitter.finagle.netty4.http.handler.UriValidatorHandler$.channelRead(UriValidatorHandler.scala:29)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>io.netty.handler.codec.MessageToMessageDecoder.channelRead(MessageToMessageDecoder.java:102)</element> - <element>io.netty.handler.codec.MessageToMessageCodec.channelRead(MessageToMessageCodec.java:111)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>io.netty.channel.CombinedChannelDuplexHandler$DelegatingChannelHandlerContext.fireChannelRead(CombinedChannelDuplexHandler.java:436)</element> - <element>io.netty.handler.codec.ByteToMessageDecoder.fireChannelRead(ByteToMessageDecoder.java:321)</element> - <element>io.netty.handler.codec.ByteToMessageDecoder.channelRead(ByteToMessageDecoder.java:295)</element> - <element>io.netty.channel.CombinedChannelDuplexHandler.channelRead(CombinedChannelDuplexHandler.java:251)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.fireChannelRead(AbstractChannelHandlerContext.java:357)</element> - <element>io.netty.channel.DefaultChannelPipeline$HeadContext.channelRead(DefaultChannelPipeline.java:1410)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:379)</element> - <element>io.netty.channel.AbstractChannelHandlerContext.invokeChannelRead(AbstractChannelHandlerContext.java:365)</element> - <element>io.netty.channel.DefaultChannelPipeline.fireChannelRead(DefaultChannelPipeline.java:919)</element> - <element>io.netty.channel.nio.AbstractNioByteChannel$NioByteUnsafe.read(AbstractNioByteChannel.java:163)</element> - <element>io.netty.channel.nio.NioEventLoop.processSelectedKey(NioEventLoop.java:714)</element> - <element>io.netty.channel.nio.NioEventLoop.processSelectedKeysOptimized(NioEventLoop.java:650)</element> - <element>io.netty.channel.nio.NioEventLoop.processSelectedKeys(NioEventLoop.java:576)</element> - <element>io.netty.channel.nio.NioEventLoop.run(NioEventLoop.java:493)</element> - <element>io.netty.util.concurrent.SingleThreadEventExecutor$4.run(SingleThreadEventExecutor.java:989)</element> - <element>io.netty.util.internal.ThreadExecutorMap$2.run(ThreadExecutorMap.java:74)</element> - <element>java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1130)</element> - <element>java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:630)</element> - <element>com.twitter.finagle.util.BlockingTimeTrackingThreadFactory$$anon$1.run(BlockingTimeTrackingThreadFactory.scala:23)</element> - <element>io.netty.util.concurrent.FastThreadLocalRunnable.run(FastThreadLocalRunnable.java:30)</element> - <element>java.base/java.lang.Thread.run(Thread.java:832)</element> - </stacktrace> -</error> - -</errors> diff --git a/narration/IntegrationTests/SituationTheory.omdoc b/narration/IntegrationTests/SituationTheory.omdoc index c94c552..a0c67cd 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:1233.42.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="fixmeta http://mathhub.info/FrameIT/frameworld?FrameworldMeta"/><mref name="[http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#134.4.0:161.4.27"/></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:1087.44.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?SampleSituationTheory]" target="http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/IntegrationTests/SituationTheory.mmt#194.6.0:221.6.27"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/narration/MetaTheories.omdoc b/narration/MetaTheories.omdoc index da33cd8..f101419 100644 --- a/narration/MetaTheories.omdoc +++ b/narration/MetaTheories.omdoc @@ -1,2 +1,2 @@ <?xml version="1.0" encoding="UTF-8"?> -<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:804.26.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://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#358.14.0:453.14.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#455.15.0:475.15.20"/></metadata></mref></omdoc> \ No newline at end of file +<omdoc base="http://mathhub.info/FrameIT/frameworld/MetaTheories.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#0.0.0:888.30.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://cds.omdoc.org/urtheories?LF"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#70.4.0:198.4.128"/></metadata>MMT meta keys and value constructors for meta annotations of facts in situation theories and (input/output) facts in scrolls</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?MetaAnnotations]" target="http://mathhub.info/FrameIT/frameworld?MetaAnnotations"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#200.5.0:221.5.21"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#442.18.0:537.18.95"/></metadata>The meta theory to use for situation theories, scroll problem, and scroll solution theories</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?FrameworldMeta]" target="http://mathhub.info/FrameIT/frameworld?FrameworldMeta"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/MetaTheories.mmt#539.19.0:559.19.20"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc index 73c6352..068c49e 100644 --- a/narration/Scrolls/TriangleScrolls.omdoc +++ b/narration/Scrolls/TriangleScrolls.omdoc @@ -1,5 +1,5 @@ <?xml version="1.0" encoding="UTF-8"?> -<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4188.123.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"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#79.4.0:273.13.0"/></metadata>A blueprint problem theory for triangle scrolls +<omdoc base="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:4731.124.3"/><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"/><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#79.4.0:273.13.0"/></metadata>A blueprint problem theory for triangle scrolls B /| / | @@ -7,6 +7,6 @@ /___| A C - (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#479.20.0:635.22.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle + (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg)</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#275.14.0:310.14.35"/></metadata></mref><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#579.20.0:735.22.77"/></metadata>A blueprint problem theory for triangle scrolls that require a right angle - We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#637.23.0:676.23.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#846.31.0:860.31.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#1946.62.0:1963.62.17"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?Pythagoras]" target="http://mathhub.info/FrameIT/frameworld?Pythagoras"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#3037.93.0:3053.93.16"/></metadata></mref></omdoc> \ No newline at end of file + We use ?TriangleScroll_GeneralProblem and demand the angle at C to be 90°</opaque><mref name="[http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem]" target="http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#737.23.0:776.23.39"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?AngleSum]" target="http://mathhub.info/FrameIT/frameworld?AngleSum"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#946.31.0:960.31.14"/></metadata></mref><mref name="[http://mathhub.info/FrameIT/frameworld?OppositeLen]" target="http://mathhub.info/FrameIT/frameworld?OppositeLen"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#2046.62.0:2063.62.17"/></metadata></mref></omdoc> \ No newline at end of file diff --git a/relational/Scrolls/TriangleScrolls.rel b/relational/Scrolls/TriangleScrolls.rel index bb88c8a..fff48a8 100644 --- a/relational/Scrolls/TriangleScrolls.rel +++ b/relational/Scrolls/TriangleScrolls.rel @@ -3,4 +3,3 @@ Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc ht Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?TriangleScroll_RightAngledProblem Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?AngleSum Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?OppositeLen -Declares http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.omdoc http://mathhub.info/FrameIT/frameworld?Pythagoras diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel index 3d24eaa..f1cf578 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/$Angle$Sum.rel @@ -60,4 +60,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angl DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?subtraction?type DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type -DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld?AngleSum/AngleSum_Solution?angleBCA?definition http://cds.omdoc.org/urtheories?Strings?string?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel index 034cb84..98a5ed6 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/$Meta$Annotations.rel @@ -2,6 +2,7 @@ untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?description untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory +untypedconstant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of theory http://mathhub.info/FrameIT/frameworld?MetaAnnotations HasMeta http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://cds.omdoc.org/urtheories?LF Includes http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/MitM/Foundation?Strings @@ -13,3 +14,5 @@ Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.i constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?problemTheory Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?solutionTheory +Declares http://mathhub.info/FrameIT/frameworld?MetaAnnotations http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of +constant http://mathhub.info/FrameIT/frameworld?MetaAnnotations?label_verbalization_of diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel index dbb5978..da2b8a6 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/$Opposite$Len.rel @@ -58,4 +58,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solutio DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?C?type -DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://mathhub.info/MitM/Foundation?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld?OppositeLen/OppositeLen_Solution?deducedLineCA?definition http://cds.omdoc.org/urtheories?Strings?string?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel index 8bbadc7..8c07a17 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/$Pythagoras.rel @@ -41,3 +41,28 @@ DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution? DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?type http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?addition?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?definition +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?exists_unique?definition +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?squareRoot?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Ded?DED?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?proofsketch?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?eq?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?B?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?InformalProofs?trivial?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceBC?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?Geometry/Common?metric?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://cds.omdoc.org/urtheories?Bool?BOOL?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?exponentiation?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/geometry?3DGeometry?point?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?ded?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Problem?distanceAC?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Logic?prop?definition +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/core/arithmetics?RealArithmetics?multiplication?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/FrameIT/frameworld?TriangleScroll_GeneralProblem?A?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type +DependsOn http://mathhub.info/FrameIT/frameworld?Pythagoras/Pythagoras_Solution?deducedHypotenuse?definition http://mathhub.info/MitM/Foundation?Strings?string?type diff --git a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel index e902a25..c90b58e 100644 --- a/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel +++ b/relational/http..mathhub.info/FrameIT/frameworld/integrationtests/$Sample$Situation$Theory.rel @@ -47,7 +47,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?C?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Logic?eq?type -DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://mathhub.info/MitM/Foundation?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?distanceBC?definition http://cds.omdoc.org/urtheories?Strings?string?type Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type @@ -73,7 +73,7 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type -DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://mathhub.info/MitM/Foundation?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleABC?definition http://cds.omdoc.org/urtheories?Strings?string?type Declares http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC constant http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?type http://mathhub.info/MitM/core/geometry?3DGeometry?point?type @@ -99,4 +99,4 @@ DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituatio DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?A?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?B?type DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type -DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://mathhub.info/MitM/Foundation?Strings?string?type +DependsOn http://mathhub.info/FrameIT/frameworld/integrationtests?SampleSituationTheory?angleBAC?definition http://cds.omdoc.org/urtheories?Strings?string?type diff --git a/source/IntegrationTests/SituationTheory.mmt b/source/IntegrationTests/SituationTheory.mmt index a81ac7e..c8898d3 100644 --- a/source/IntegrationTests/SituationTheory.mmt +++ b/source/IntegrationTests/SituationTheory.mmt @@ -10,36 +10,36 @@ theory SampleSituationTheory = A : point ☠= ⟨0.0, 0.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "Point A" + meta frameworld:?MetaAnnotations?label "A" â™ B : point ☠= ⟨3.0, 3.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "Point B" + meta frameworld:?MetaAnnotations?label "B" â™ C : point ☠= ⟨0.0, 3.0, 0.0⟩ ☠- meta frameworld:?MetaAnnotations?label "Point C" + meta frameworld:?MetaAnnotations?label "C" â™ distanceBC : Σ x:â„. ⊦ (d- B C ≠x) ☠= ⟨3.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "distanceBC" + meta frameworld:?MetaAnnotations?label "BC" â™ angleABC : Σ β:â„. ⊦ ( ∠A,B,C ) ≠β ☠= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "distanceBC" + meta frameworld:?MetaAnnotations?label "∠ABC" â™ angleBAC : Σ β:â„. ⊦ ( ∠A,B,C ) ≠β ☠= ⟨45.0, sketch "calculated by ComFreek by hand"⟩ ☠- meta frameworld:?MetaAnnotations?label "distanceBC" + meta frameworld:?MetaAnnotations?label "∠BAC" â™ âš diff --git a/source/MetaTheories.mmt b/source/MetaTheories.mmt index 517507d..cb2ec21 100644 --- a/source/MetaTheories.mmt +++ b/source/MetaTheories.mmt @@ -8,8 +8,12 @@ theory MetaAnnotations = label â™ description â™ + problemTheory â™ solutionTheoryâ™ + + /T example: lverb ?fact "default text" â™ + label_verbalization_of # lverb â™ âš /T The meta theory to use for situation theories, scroll problem, and scroll solution theories âš diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt index 0d5bf59..71f4c89 100644 --- a/source/Scrolls/TriangleScrolls.mmt +++ b/source/Scrolls/TriangleScrolls.mmt @@ -13,9 +13,9 @@ fixmeta ?FrameworldMeta âš (nicer image: https://en.wikipedia.org/wiki/Right_triangle#/media/File:Rtriangle.svg) âš theory TriangleScroll_GeneralProblem = - A: point ☠meta ?MetaAnnotations?label "Point A"â™ - B: point ☠meta ?MetaAnnotations?label "Point B"â™ - C: point ☠meta ?MetaAnnotations?label "Point C"â™ + A: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?A "A" â™ + B: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?B "B"â™ + C: point ☠meta ?MetaAnnotations?label lverb ?TriangleScroll_GeneralProblem?C "C"â™ âš /T A blueprint problem theory for triangle scrolls that require a right angle @@ -79,7 +79,7 @@ theory OppositeLen = meta ?MetaAnnotations?label "OppositeLen" â™ meta ?MetaAnnotations?problemTheory ?OppositeLen/OppositeLen_Problem â™ meta ?MetaAnnotations?solutionTheory ?OppositeLen/OppositeLen_Solution â™ - meta ?MetaAnnotations?description "Given a triangle ABC right angled at C, the distance AB can be computed from the angle at B and the distance BC" â™ + meta ?MetaAnnotations?description s"Given a triangle ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"} right angled at ${lverb ?TriangleScroll_GeneralProblem?C "C"}, the distance ${lverb ?TriangleScroll_GeneralProblem?A "A"}${lverb ?TriangleScroll_GeneralProblem?B "B"} can be computed from the angle at ${lverb ?TriangleScroll_GeneralProblem?B "B"} and the distance ${lverb ?TriangleScroll_GeneralProblem?B "B"}${lverb ?TriangleScroll_GeneralProblem?C "C"}" â™ include ?OppositeLen/OppositeLen_Problem â™ @@ -91,7 +91,8 @@ theory OppositeLen = âš âš -theory Pythagoras = +// Doesn't typecheck, not sure why âš +// theory Pythagoras = theory Pythagoras_Problem = include ?TriangleScroll_RightAngledProblem â™ @@ -106,7 +107,7 @@ theory Pythagoras = â™ âš - theory Pythagoras_Solution = + // theory Pythagoras_Solution = meta ?MetaAnnotations?label "Pythagoras" â™ meta ?MetaAnnotations?problemTheory ?Pythagoras/Pythagoras_Problem â™ meta ?MetaAnnotations?solutionTheory ?Pythagoras/Pythagoras_Solution â™ @@ -121,4 +122,4 @@ theory Pythagoras = meta ?MetaAnnotations?description "Deduced length of hypotenuse AB" â™ âš -âš \ No newline at end of file +// âš \ No newline at end of file -- GitLab