From 67ee16e164d79aa34eb80eae68a88bffd64b04ac Mon Sep 17 00:00:00 2001
From: ComFreek <comfreek@outlook.com>
Date: Fri, 4 Dec 2020 18:13:59 +0100
Subject: [PATCH] rebuild and ocomment out non-working gearbox theories
---
.../FrameIT/frameworld/$Opposite$Len.omdoc.xz | Bin 2180 -> 2184 bytes
.../LoViVo/gearbox/gb2.omdoc.xz | Bin 1396 -> 1216 bytes
.../LoViVo/gearbox/gb3.omdoc.xz | Bin 568 -> 568 bytes
errors/mmt-omdoc/Library/gearbox.mmt.err | 180 ++----------------
narration/Library/gearbox.omdoc | 2 +-
narration/Scrolls/TriangleScrolls.omdoc | 2 +-
relational/Library/gearbox.rel | 2 -
.../http..mathhub.info/LoViVo/gearbox/gb2.rel | 38 ----
source/Library/gearbox.mmt | 11 +-
source/Scrolls/TriangleScrolls.mmt | 2 +-
10 files changed, 30 insertions(+), 207 deletions(-)
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 1341ea63765389c209fe268c185289f84666526c..d49c48d3553d1fffce76a592b328f9b419d399ff 100644
GIT binary patch
delta 1853
zcmV-D2g3M-5r`3x8Ut4dN3k7C0e>j;P4ql^eUo@<-G_lJoHfMDT~Z9^7)&blZ-s9j
zxLR(+4W8Q|Egs2;7qjO7*hXzZR?mqGt5g)EH-Hf0h9k(l?rLU34McRd(6qiV^VZmA
z(M6Shj+Gz!(`u!}N7=-joVkUg6;DV^F$XWm<Hh;<rM!(V?GgZ2{&N^~B7Yx<i-PIX
zK1n)6BGCm9XH(GJ!OVon4#nhOx7zUKp`;7I3i9So(LK@agJRUjjhvmA9s@G9`rGmX
z3UOXQ0hxZ$C%p_}NqewcO%81Mf|hL|Bj=0WcF0G4>oZ-Fpr4(!EM-rKZj-DFs4iB9
zc14a)&ESWT687T0mlM;r5q~5c<K4()_G{p4?;5pth$%mP5=lLLk+c74#(5#-IT`7O
zGHxcLLNt_5aZwfLN8=NSywi~MIC%9hW+FZx?s~l?XV(xg=8+qzBZ`HHLA3PoHrDtl
zaikLj*A$%LoZ+u-hwAJydcZFokf&=3>hgoqbJB2fo-$~SS-BvNoquhlO5m19WrH53
zR6uV`sf?xUD>61UwKDAzgluLLnz{Jxp58-z;uvBj#Ow(I>vEB?sKjIYtpHi9ks~vi
z9Y^#e<o%csa`RE#OCwA39wHC38J-qMh(CF!79I1ckinaY$XdT`2sy0}A9;{Fw{XC5
zU@mxLV&wie&lWRnoPUYdYv26pyV#<#EnW~>jO1@^Hi1RJKw&L!Xq<<-!(=utLYnc4
zDUZm_1JvuZZW)^xC$nbQWK#^+^o7U-4{DIkN}Fk_6tbJHX3z5#8wPdZ3;+&7?>1FC
z60JQMYb-DhJ?I1>-v|a8RsDmicnMtp8KNQbe8fP5<G1@eOMjYQMKn%JcuP}#nD&v^
z{{TanpZBD@BrX9=*_hZkR$e`urBFHKrNN&BFFLLq7Ck{IKQ49^jF!(j*V{@;J3@)U
z+l||!kzQoNA3!KL^c*3QBUd;>;XR@9UY42eR<#$uY%rwe3*WL^g38@Y3alWOtPr&$
zfPnNPeD~CH-G9%zO*0~3J5QB*;SUVG2P1~1_^|3!D^Xbnb?G*!@xN`H+gHy)AAOWM
zh3v<fbnDj<<D~OQ@EoWrkchmOhfhrXqPtZ!5Z~ZKm#!LwRz{~0B^$~yI^&Hg%aXoW
zZ>_5(zP@2R`>j@QLx<LQ8r_Ge!HvqOCAzjU0@1L5+<y<f5o3qJ7@s0yks!bxX*oW3
z9`Sde`&!~g!8dQx&%x{MZWjQS9JI{z$cO58xb?r2k&<K^GMPtL#s@nTIn5Z;I%j>u
zP+etELK$c<!OatvKKd~9pQz<yg1lA|<4eN2b4c~TIc7q2EyjYTe(k`CUZG)Mrw^L#
zz*aq?-+vKR#!WB|ruE6R&GU1Z(+LlO8ZV>|F~`XErDz|)V)^}~SV|aXwF#pL(0Fmr
znjXZc?e>_Texgu@r5crg_b*K3BiN9R%DyG1zE4+sVb$!xpAt*=rJ%4~yb$O4gf(rT
z`Bp*-iIXSn`MBtcbMZ2H=gMtpXsgfVfm2`nIe+p9t)0BvXqUy72~@qjA=nz(F);(N
z2xErHG#oB5A*A+q1}2%Uh5T*+oj{DApq1<prghT*qFLuohYCPUY`qLal(!BNm$eJ*
zQWZm#()|}W>Wb2+<xMRa{J|g~uyv%UZkl;Rzg<&9%2rmH=dKPBKx2U&%}ygiDr0BN
z=zkPrAuH-&4A5`%@VG@QTw>lNRcX;JQ52nov%W$Ml#Fa{mE_qdWP86_#_t3tJP=fn
z)HZ80nqsOZ9g;u)zpdKd4Jp`1EHb{2x6=J-a##;o3lfrHd{-}~yZr(_h&GEm=_T^i
z{}-SwuPAIc1%KM#fk(i=U#B{m>3q_K34eahjdkI+yG_L}{E%ZLx0*>;;*AaUD)2?Q
zeB*L{(kD$O0sI(xt*^RV{yitPi7AITuW*LC=M{5@lC&}qjqE=@S(-}cIfKR1i?5Xw
zmzXA_I8eB5ao6C487908@5MO$0xHYBOvrpvg3tjSY4gFGNhR@JWP&*y^8tmpO@F{l
z#dF+Nh;QB*)bLY<7F*xyI;X)yhR9Yd-z*0J)+gqVqqotx*}Hrt9$srgJ5yWOrZMp%
zvqo{HDpd97@TX>j%*eIAGtmol3OIEE6!(6GXI~+m0~tTZ(+8gMsV1|B7sp`UfRGD$
zb_{yyf|@$&<{-;5qV<>fj;i!UWPdB{sE-4IX1rs~Ed=0wih1+O6j-IgZ2o#&g~Veg
zrv)1+AbqbJO+t$^*0lw1N%9_`(9#>|?RTxa&C%8Y*vRWSmD&({-k-r4yL;Zk5GOIv
zu0KZbA<!uk8!o~4c-AY<gXSckrvnJSp0&TkO!NtU><3V98QwZPsJ6SF!!EUYRxktZ
r;uUoTRS^IHv9wQb;UFds00H9=*rEaeiBL~CvBYQl0ssI200dcD#)^mQ
delta 1849
zcmV-92gdk_5rh$t8Ut?#L$Mu80e^*bdT<HG0Bf4N>0`7yK^4Bm>!LEcxVh9rVrC)W
z^jN1T*u$%60!$bFz!TS!ZL=L8dK4^zF}|VUWty+R_|#$PS*Lmz^9RCE=aySm=}mhn
z>uppyo<ir+MO)xZ9-2S0tc&^jZpMg_w_6gHf&H$fsKQ?#P}yr>IRGC~!hfr|oz{pa
z27-jAGlmEQsa*Swurvwm?o0Mwx6XBxVmQVfGBI+MYcW9{)$wP5bBB-RZ9`-X-Cxcm
zI`zYMH}Buv{FUp~cxl)K28DxH4rBLQ7B*}EgT+C!xGa7}YG(-qRzg691T44>O!=%Q
zA{V;h9c)W>OEd!34g6J*+<yb!9O-6gzVSIGAoAGnSrmYn;)j=&DH7Itwj%Wz9kt$>
zB5eIB0~H6qlB5WD?SGFgiFS+S#KUOW4p2~P4)0qNC{h8>z-q))V^MgXJO^DLw2x!m
zoF<QxMZ-Zx`reWhR)hawNEfbbwt`SF^2*f3yD?I<swV50hsSn0+<#t?MN9X~6+|%0
zn#l0t<+esNEql-q80@2a6>n7m3I>tHm@oQ=v)riIOQ$cpTFq039v<!o$`?(43_MCA
z)(-4Om8Z!*;+8z8jp7f&kBBPWu<W|s+|tldQ0$a?&FWTdX7kY*bqE-&YT-CiMSu#;
zx=8@uI1$w|#`YjqJAbg~d8g{BIAe$o>V><{dXjM-<2!}dp6Hr{&_U;3?&-Vo<bP%Z
zgL|mKkM${a&4DszFdQ2`ix=AUwmfRI(x!ydKg=4(sjWSXyt-rKw-G?#mKyZ5AQzX3
zPJ%Z2njll8O)>$sg&O7P=HyjAHyDIc_!$A+cdo-E^b9*qy?@Bn#z8BJZ4s^X^v$H}
zvL2N@1-W&XCi`pIC;FMyGv%2qyz)vGj6ufT@vF4b#byK}lZ^66*1hjYbsMXyC4Qft
z7z-1^d$PROpWr2mZbSJ9ofx!y$qDKqAEEkUPWdxVO7HgV9Sn-fQk`8t|0qAe*6hmj
z;db7!7wdo(AAc6InJ?Eo7u#%emrE^sf9|=^P6OQXn&02BTtdq6T&7dv=~agg#&}LV
zpA(RwT-y$OBfrX@dY@k6&{t{>II}Xq_Jqg5UYU(}&v&U>Hive-cCzOUj+ZmP*T2ep
zE+g7l3IUD3Y7X*!ouYqQ!$Y`)wQUHILup4b6(?1ZcYjq`GBq|X=1o=)NLmA9xOrhL
zeJ*d7)AOAY%eq?=cF9})Z|$8BeUZ~Cmi+U-VV*w0_y5X&9o67X2Yg=h=X;)<>LK33
z-%`Zw)JUd`LV24%URwwMiD+7%VU-rcrf2d0uErU=3*J|J%pZVW9##*$DlG7Mn?eC1
zvS2}zV}JXVdX65Is=(veyTL_%HCw24rNwnXh0Uj@$rOWI2*>nnnxr4&qAdc${fhD$
z1cpR`bXvs76V`(z0Ng_q1>Q4XbH45FpmKs*O!CdI5dHq)I>qm$C?-L0LXTt9Gl#XT
zaS-tm`^BfceE*bZ>zz%i%A9>mFn<Y4>4nK3FMs;A5g@RvF_GO9aK29x{nDK3e=MQt
z6pCUXC_AP>gN7F6-`Po}qR-uF8eKigKkn$P_dWGgV51>DmCB`8;Jh{^y3C@2ALr?+
zyAS&K2EXEy<@@)qp9zHgcw8+lJSE{$h0>H;mJXDT9n#orv$1DZ4)&kvqjFM);d`h&
zRDUG79gXB$!kW$kp@1?BjS)Y}is${9!106$ET^tEAOmc_YIrns*2R&V`M#w|9xyX<
zENKU;d3MPRPbY~uo?u>Rv(;HEDL1$Samt%MTlP*u<bu^+FkO8_P726_8H1rd<**I!
zM%B4z*ei!zihlHx^^X%dwvhufE`hD+V1Lq0Yu(Mo02!F@e=k82jC>T=7#68ZN%I0s
z*P3DSP^Zp{LhAUp;Enp$QH6QPmSXi;U2ed316Il54{sHjhY#L_mac^<LSgtIsxXkE
z9pl}r(3LVIQlSXP#rA-RZ;A+bzErKklKF0l_N}4ir8)rL^es|8P>$fMmMuabdw(G0
z8Vh#|=Ts~y897y`{uXa{<HG?@+KjHCufwoYjOZCK_fb+yY3#e+X?jJi0&A2)pP}v9
zNA<t<`pwq`f259JPfAMAXhoUf2U9aI1UH7V8#KkdaEJlF@TYVlJL$O^(JJ;9?cuMY
z(>u$JMj^I8N0cQzl5%*PGG>>SB!9xkCc!tTFrgaBfA*dyOJ&S&-tpk3ixto^x{N*5
zSgJ|+Jo2a+O6PAe+qyeS&losW$N|U)?{_21`keLIdmFb{JzHJL*k+4Vzja1c)Upi7
zGHo^f50QzH0PM<j_O7{3Kh}wuW(J%mP0VVUp3|c3WnE*A1u>85LHFs$2r51RQT?EN
nS4aQ=jB_fe(KUBB00G|+@S*|$ju3G!vBYQl0ssI200dcD+kKp-
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb2.omdoc.xz
index 7f416c6aead594fad584456104d1195c93a2c16c..debafb33bca360d222942c21fcf8689d70c71f62 100644
GIT binary patch
delta 846
zcmV-U1F`({3cv}F83ZG$1c0#}YXN_BWsS2e>5pBeVgsQI`<NP4rHG9q7-<nGA{TrY
zi}hRkef&f%7^69M=AxlWWOPM=O9DK7*HfsncHvnOAsfUdFtdPmE@Pzuv`qCVt78{K
z{~nGaisH5iM=;QAdR+1TxIhiUROH}v0rG4&h!w3B=K-2hP1Mq<T}rk`l5c+*qmPdU
zXeBrbqQ+o$scl!jECs<=o18d3gg}0~Qu5h&X*&esLE0@b*D!f+TRnnj$$6Afla>o}
zdvQ_Lf#ZmV9Y*_NBA(G60wHJ!^{P^3m^f)vKohtyb6?Jl>&mmwfqxi_0Ng7_D0e9C
zTCWSa>|*3*SH=xrv^wXChz);(C*yd|&Zz2{QE-0J`jI=`m+G+Lpv+YH;f@!2^138F
zPR(GKYG3p3s|5}63FMLvd>JIMPo0V@z4P`oekDF7JW;`bOh;d&15B)S^HPONRN^O*
zbt{u|>BcGxvP3#;H$=yvOwK28!xY6+kl@ds_RBi3QIKnGLtn4!loEefO_AyB!C>Ur
zW8}Pi-+GpNHr{3E@~tR+C<fpIOHXYkT2;t0@j?k>5-VEy#uN~5GpXikBi{Zd0@w!S
zc->hTFb6E*Z?81XJxI{zs5H$Q2}3CTT#V$WkK_SE0zu`7v$?7HkMe?L34-I6CTd*?
z_+q@Dqv-7B8GjVHRSkda!rsjGsK<{n*QtpJ0W&^9e$=ZBb=<x``iSw3MA_Ojt0uH?
z70eG$9zcj6!gJC#tg+(%jcHEm8Gstx0nTfw)gv5_xQ5&gkm{jmjdCSyvdT_ScvJrR
z=bU@;XL3c&XPrP=B%-~h#N!4f+CTCb5-rJ!S+M$^BzNz`e;a?B_A3j{9rdM~<iclH
zpC};}i53dq;V*GNkMGcLb3rtUY2Z_G_+Z?h+G5V1Q8)=H`ad&qB>76Jvm8;0(B))8
zFYq1SUQo6`UVQ!O9>UrJP6B<O=u(ItGUjKN5*${pCmhef_%-DXjw!I`&pYA+Yt*s8
z52VEcKj-Lg$FDwE+618#+&M+IBn$#R5+4w!hPj?{@IY=R>)Uye0EX|zGf<=sw*Ud0
Y39Cl{0M%t)OR>af`vL#}000D8T87D!iU0rr
delta 1027
zcmV+e1pNEJ3G@n(83Z?>1vIf8YXN^)B2|g#^>p<u?hK^DK9de_#@@X2doFK@AEryl
zr8iT$3q9{B0#AscGP>*e_E=>JUTFuI<(G1i!O0gccu@5VujbpzNcxJ}K33ddJs4&d
zn3Sr+D5OkM!C)saya<nl5^Xg951TAc5sn-((q62R24&nRz3zS%=q&LH6s>=#nZ!AQ
zG3;1Y>9xt=Y6Qy&nUtwz>#WHdr`~$EreYB+qR(n|LmhE$j&l7}XRucLOh}#zthhWe
zgel@bDO%O1dht<#J5svGEu8ZV#`!Zx)4GwINvTRng7F!Kk5y|oLr}EYwUQXBMTDnv
zUXO2$*=MJ11jSSgn7MCI4>o^vx*q7z&Znp5;sBvKUt-qs>G!)gGFY-R)SIu=B-c4B
zZ9@P#0x70CM=~Th(;TGBPM1NP3X4F4yEe6$H>(;2W9i6Fw=A-hXMp?3S!EpJ>17FT
zNpEZOqd%6Z_kA0m@%SGQ*i>b%<w(<C_O}um&7XpQU!Gi?`&BufBMN`fSM56!u&B$F
z%Yg}z34A$+E;~V$b>h?Oce-p3&kV<5vNK%X4~ih$l>hL`l%f_@kVA5FAfb_<aRb0X
zFa+ZJUSjo4!S~W^ico?iL7p09V<!^)Jn*_XM1s--I)A@#Q-G1Rt;#HFU4R*6-td~o
zN?@0{_PCiqDN5=fh17qzmZ*O@3#(vdMiEW=bSTMzw6!bM=gX5Eu@APuo=98F-Auq!
z8~=w}nq~7jjs>dJy?{sLEO~j{hq)Yzo0en+4T4BNhEoJ@Y*|xv<WZ;X3*tz{qTnk{
z9epL4>~+xmvbem5n$zRkQGPULhm73L?BWPAT1RIJWc<XhaJhe_9;Z-AVCL+E9J@W+
z87A0xMCA3MrMOaUDjK=+#|Zawb5-qv6!aw0f=`a=p&kh%5&&`tBN^2Na?y}3N||@a
z^T~aCm-%!^ORGe(CY`EEVktFT9j<taYr(g2?TXmzG&J3bDlGfb#d3Wr+kr+%GlvGn
zL09NGdR5fP%7=e-r+vCTnd++A)&}nj%rOt~+BUHK<_}}F)c3S8NE8|KSmc49Qi9pL
z42b!rYC*yW)TQUJW|_6)DLIIufy*c}>hqncojv9{(w*g<iHn4*_^Z5+d<wMx6N!~d
ztsB$Al={>Q9iC^n5xjyd0?+F)w+_IZPI{IdQXmeY4iR(L=qjfY^TbV2_yk>=z(O3#
zl3p7m#3Sxe@$Oi)$0}$<ivO;!TrT{8;)0<(#N&w9+EmE>+}>g)!fe{7WoPb$EgCG8
xK3l%mI_6Oe8k}#2005fg&_`l5!nFVa&<dh&006*^GC#4zXZr#G00004Sy~6@{5=2w
diff --git a/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz b/content/http..mathhub.info/LoViVo/gearbox/gb3.omdoc.xz
index fc8667a1833e2db7d8620e35a7fe1399ebc4b702..671b5fa992b92326bbc8b579c8427779c1700366 100644
GIT binary patch
delta 174
zcmV;f08#(A1h@pSe*u5@Mc1QP*T81v!he6-F-n~6KH@l(v8O8aVY9#Zb;jQIODo^?
zM;w>%q~IqQ1iy@h-y4fdjgGS%q>iN@)+^T30&R9+_Om`yUocZ=86Fx%ESI>YWwNj?
zT~0!F8h|sEZNHRnmwY-98ru?#y;eUT6@tU3y<<s&&#bYS!|ftLeEI=iUuXH&pSDLj
c)%C1@hPWkU6QTeB09i0OGV<TU`ja367(7!{qW}N^
delta 174
zcmV;f08#(A1h@pSe*u5kihjX4BbR;;a0c8pV*1P%cB*5L`^%`F<f-rIXR%Yp_}u`O
z=T<MwC(0m29BMLFMXj$`^kMEoe$5zn@T0x%u3p*ct~ulue4Q7N3^fYoZv)PK_L<}2
zfSHrSGydSle{Deft*eyCnha>x<W9jGmvU83+MGd*M<jWG)aD{HRkcAF=P6#9<I``h
cn3bbc?>{5{l==Vw08<)>#Qfd036mfK7&hWr;Q#;t
diff --git a/errors/mmt-omdoc/Library/gearbox.mmt.err b/errors/mmt-omdoc/Library/gearbox.mmt.err
index 7aceb81..8ad7b1b 100644
--- a/errors/mmt-omdoc/Library/gearbox.mmt.err
+++ b/errors/mmt-omdoc/Library/gearbox.mmt.err
@@ -56,11 +56,11 @@
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
<element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦y.radius≠0" level="1">
@@ -121,11 +121,11 @@
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
<element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦x.radius≠0" level="1">
@@ -186,11 +186,11 @@
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
<element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$2" shortMsg="invalid unit: using default value to solve ⊦RC.radius≠0" level="1">
@@ -250,151 +250,11 @@
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
<element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
<element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
- </stacktrace>
-</error>
-<error
-type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?c1?definition: Judgment |- ['center=⟨0,0⟩,radius=1,numteeth=10,angle=0,angular_velocity=1'] : rotating_cogwheel" 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$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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.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.tryHandle(ActionHandling.scala:69)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
- </stacktrace>
-</error>
-
-<error type="info.kwarc.mmt.api.checking.RuleBasedChecker$$anon$3" shortMsg="invalid unit: http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?definition: Judgment |- eq_refl c1.radius+c2.radius : ⊦interlocking c1 c2" 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$15(MMTStructureChecker.scala:377)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.$anonfun$check$15$adapted(MMTStructureChecker.scala:353)</element>
- <element>scala.Option.foreach(Option.scala:407)</element>
- <element>info.kwarc.mmt.api.checking.MMTStructureChecker.check(MMTStructureChecker.scala:353)</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.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.tryHandle(ActionHandling.scala:69)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandle$(ActionHandling.scala:67)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandle(Controller.scala:74)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine(ActionHandling.scala:64)</element>
- <element>info.kwarc.mmt.api.frontend.actions.ActionHandling.tryHandleLine$(ActionHandling.scala:57)</element>
- <element>info.kwarc.mmt.api.frontend.Controller.tryHandleLine(Controller.scala:74)</element>
- <element>FastREPL.handleLine(REPL.scala:68)</element>
- <element>FastREPL.run(REPL.scala:48)</element>
- <element>REPL$.doFirst(REPL.scala:34)</element>
- <element>Test.main(preamble.scala:55)</element>
- <element>REPL.main(REPL.scala)</element>
+ <element>FastREPLExtension.handleLine(REPL.scala:70)</element>
+ <element>FastREPLExtension.run(REPL.scala:49)</element>
+ <element>FastREPL$.run(REPL.scala:38)</element>
+ <element>Test.main(preamble.scala:68)</element>
+ <element>FastREPL.main(REPL.scala)</element>
</stacktrace>
</error>
</errors>
diff --git a/narration/Library/gearbox.omdoc b/narration/Library/gearbox.omdoc
index 5f1c1c7..7a6448a 100644
--- a/narration/Library/gearbox.omdoc
+++ b/narration/Library/gearbox.omdoc
@@ -1,2 +1,2 @@
<?xml version="1.0" encoding="UTF-8"?>
-<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2550.72.68"/><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/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb2]" target="http://mathhub.info/LoViVo/gearbox?gb2"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#1897.53.0:1906.53.9"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gb3]" target="http://mathhub.info/LoViVo/gearbox?gb3"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#2448.67.0:2457.67.9"/></metadata></mref></omdoc>
\ No newline at end of file
+<omdoc base="http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#0.0.0:2736.75.68"/><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/LoViVo/gearbox"/><instruction text="import base http://mathhub.info/MitM/Foundation"/><instruction text="import arith http://mathhub.info/MitM/core/arithmetics"/><instruction text="fixmeta http://mathhub.info/MitM/Foundation?Logic"/><mref name="[http://mathhub.info/LoViVo/gearbox?temp]" target="http://mathhub.info/LoViVo/gearbox?temp"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#178.6.0:188.6.10"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?cogwheels]" target="http://mathhub.info/LoViVo/gearbox?cogwheels"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#359.13.0:374.13.15"/></metadata></mref><mref name="[http://mathhub.info/LoViVo/gearbox?gearbox]" target="http://mathhub.info/LoViVo/gearbox?gearbox"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Library/gearbox.mmt#839.31.0:852.31.13"/></metadata></mref></omdoc>
\ No newline at end of file
diff --git a/narration/Scrolls/TriangleScrolls.omdoc b/narration/Scrolls/TriangleScrolls.omdoc
index fd782e5..e0ac541 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:4945.141.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><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><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#128.5.0:322.14.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:4919.141.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><opaque format="text"><metadata><link rel="http://cds.omdoc.org/mmt?metadata?sourceRef" resource="http://mathhub.info/FrameIT/frameworld/Scrolls/TriangleScrolls.mmt#0.0.0:47.0.47"/></metadata>Modular scrolls having to do with triangles</opaque><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#128.5.0:322.14.0"/></metadata>A blueprint problem theory for triangle scrolls
B
/|
/ |
diff --git a/relational/Library/gearbox.rel b/relational/Library/gearbox.rel
index 29e4c7b..8474376 100644
--- a/relational/Library/gearbox.rel
+++ b/relational/Library/gearbox.rel
@@ -2,5 +2,3 @@ document http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?temp
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?cogwheels
Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gearbox
-Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb2
-Declares http://mathhub.info/FrameIT/frameworld/Library/gearbox.omdoc http://mathhub.info/LoViVo/gearbox?gb3
diff --git a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
index ee58104..8f75ff9 100644
--- a/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
+++ b/relational/http..mathhub.info/LoViVo/gearbox/gb2.rel
@@ -1,16 +1,10 @@
-dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c1
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2
-dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2av
dataconstructor http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
theory http://mathhub.info/LoViVo/gearbox?gb2
HasMeta http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?Logic
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gearbox
Includes http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/MitM/Foundation?NaturalDeduction
-Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c1
-constant http://mathhub.info/LoViVo/gearbox?gb2?c1
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c1?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2
constant http://mathhub.info/LoViVo/gearbox?gb2?c2
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
@@ -20,41 +14,9 @@ DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://cds.omdoc.
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/MitM/Foundation?NatLiterals?pos_lit?type
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?definition
-Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
-constant http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?NatLiterals?nat_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gearbox?interlocking?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?Logic?prop?definition
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type http://mathhub.info/LoViVo/gearbox?gb2?c2?definition
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2av
constant http://mathhub.info/LoViVo/gearbox?gb2?c2av
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2av?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
Declares http://mathhub.info/LoViVo/gearbox?gb2 http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
constant http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat
DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?type http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?Logic?ded?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gearbox?compute_av?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?cogwheels?rotating_cogwheel?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?proof_interlocking?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c2?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/LoViVo/gearbox?gb2?c1?type
-DependsOn http://mathhub.info/LoViVo/gearbox?gb2?c2avcheat?definition http://mathhub.info/MitM/Foundation?RealLiterals?real_lit?type
diff --git a/source/Library/gearbox.mmt b/source/Library/gearbox.mmt
index 3c1edb3..ada38b4 100644
--- a/source/Library/gearbox.mmt
+++ b/source/Library/gearbox.mmt
@@ -51,13 +51,17 @@ coaxial_cogwheels : ⊦ ∀[x] ∀[y] coaxial x y ⇒ x.angular_velocity ≠y.
// a particular gear box with two cogwheels, one with undefined angular velocity âš
-theory gb2 =
+// doesn't fully typecheck (probably because some computation rules, like for sqrt, are missing, overall non-critical errors âš
+// theory gb2 =
include ?gearbox â™
include ☞base:?NaturalDeduction â™
+
+ // vvv doesn't typecheck â™
c1 : rotating_cogwheel ☠= [' center := (⟨0 , 0⟩), radius:=1, numteeth:=10, angle := 0, angular_velocity:=1 '] â™
c2 : cogwheel ☠= [' center := (⟨0 , 2⟩), radius:=1, numteeth:=10, angle := 0.05 '] â™
- // should work: â™
+ // should work, but doesn't typecheck: â™
proof_interlocking : ⊦ interlocking c1 c2 ☠= eq_refl ((c1.radius) + (c2.radius)) â™
+
// ...but needs computation rule for sqrt â™
c2av : ℠☠= compute_av c1 c2 proof_interlocking â™
@@ -65,9 +69,8 @@ theory gb2 =
c2avcheat : ℠☠= avc c1 c2 â™
âš
-theory gb3 =
+// theory gb3 =
include ?gb2 â™
-
âš
// we want to compute an update rule for the angular velocity of c2 âš
diff --git a/source/Scrolls/TriangleScrolls.mmt b/source/Scrolls/TriangleScrolls.mmt
index ba7b636..80086b5 100644
--- a/source/Scrolls/TriangleScrolls.mmt
+++ b/source/Scrolls/TriangleScrolls.mmt
@@ -103,7 +103,7 @@ theory OppositeLen =
// the description verbalizes deducedLineCA, hence must come after its declaration â™
meta ?MetaAnnotations?label "OppositeLen" â™
- meta ?MetaAnnotations?description s"Given a triangle â–³${lverb A B C} right-angled at ⊾${lverb C}, the distance ${lverb deducedLineCA} can be computed from the angle at ${lverb angleB} and the distance ${lverb B C}." â™
+ meta ?MetaAnnotations?description s"Given a triangle â–³${lverb A B C} right-angled at ⊾${lverb C}, the opposide side has length ${lverb deducedLineCA} = tan(${lverb angleB}) â‹… ${lverb B C}." â™
âš
âš
--
GitLab