From 006a3d2317784e486eab1f19c660a1672a2ebe6a Mon Sep 17 00:00:00 2001 From: Aaron Tomb Date: Tue, 28 May 2019 16:25:10 -0700 Subject: [PATCH] Mark muliple-goal commands as experimental Due to issue #316. --- doc/manual/manual.md | 3 ++- doc/manual/manual.pdf | Bin 375887 -> 375980 bytes src/SAWScript/Interpreter.hs | 12 ++++++------ 3 files changed, 8 insertions(+), 7 deletions(-) diff --git a/doc/manual/manual.md b/doc/manual/manual.md index 23c9b9cd70..1f9631d7b7 100644 --- a/doc/manual/manual.md +++ b/doc/manual/manual.md @@ -1246,7 +1246,8 @@ immediately returns `True`). It fails if that is not the case. The proof scripts shown so far all have a single implicit goal. As in many other interactive provers, however, SAWScript proofs can have multiple goals. The following commands can introduce or work with -multiple goals. +multiple goals. These are experimental and can be used only after +`enable_experimental` has been called. * `goal_apply : Theorem -> ProofScript ()` will apply a given introduction rule to the current goal. This will result in zero or more diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf index 6ede224850ac8c772f1f204db7c05d6141adf4f2..dcfec8152e8ec93ff64ad4b3d5e2d85996d62b7f 100644 GIT binary patch delta 7385 zcmaiWRa6uJyDi<_Lw9#K($YC}cMaV&G)VU-Axgs#14>APG(!m}%>WW23?Nbx9{+RJ zUH3fPweG`y*zxwQz1KH?N7Zys755R<5`ZQx1z8+MxW6D!~X zsWJqnPh-wguFU7oP=~GCK8BLwzQOw=?b%}xi-T@wd!}{~6LiV;_*loG+f@d?-MSuw zcA?Bv!ok{fHhyR|t}b7EY<@>FJkmdZ;QP5TX3Rr*vw=n@`?%mk#d=CDihE8aN*MI$ zjel}oI|qGeIj#R`aMuv9qqN0ee8GRRQXKhAR(kijG?|3;5qI6`^5?a^kQ3(!v`Z8> zDNWRwowch_>l9|)DE?)fEL4dAXpiKxS?ApC_-bP@>IX@#eDOP1Btm{13yClN(MQUKB4vKWPYAH{Jl^O zdhj|jpR@`j%?$2QE5T$8ob zm6H#}k-orV?p`AbgNnMLph)QfNh8^Vr9D3+&bH=2hGMuJ=ee6wDd!hH{_guculMk3 zXF67nH9tG8+twh|N4MH=-G72D)`~5b0i2HsTd4xuE9Rt1|jviv!@$zB|b41~Xkf zG2Z%C?MN#fl0<3EM_Y#0%+>e3fm(z;H%xw5fQw%xa| zCu0(F1{bDlnW%@)teY1Be5YX2It>jpI3q`a;+kfCBcF= z(31n*vmQrtc=w;U__wnL2qr7vpZAcLxl)v?t7*95C4m1q8b)KO(r2qRkuMbT$$l{g=|1(3Zah~W#8;u48X_wgW)2Nrjbp=6#GM< z{%~HGy%6ynhW_ZT>W*w!4A_jeCF7@u|)TU#EPJ?Qbg6MW29!3WsZe;lMA z_`O$9org-0^&QF41Ak9kA4CSFBxdg?nyg}W0xk>FmIY~ccG@n(*Uy>XzufO23bYaOY z6CJm*Vki}KRl#vg01Hgu-@TAWAF5>mg~Ly{a53huinhDdC7LoO$Bt79qlAd`?%`)N zIL!x_tYsDANi_yV%CGg;h*ym$q71%JKJ?8#yy_0-lJp3{_|fA|bB5s2V95xsd=#!8 z!d-V|R&tWPF5qSbvBNjFC~e{M^VUsZocgmA@wL^_TUH{q>2JXB)X=TU7YRDl>N}h0%|xu5 z`QI)hC}`vGx~QZ-u`kIAO!ZQOBmP!ib4a7JTt~O7x(R%c9`#(?og#QG(v6qno!DL^ zaLp_GF@Zj(HrM|=CcBhSQbi?)zEqx!hIbsP`4pVmO}z8b z&OVVzu@j`SJ}BI!3%$$

+AV9ICi>b>K9r<1%y*tjJ(xY99XbGqeO2G*-KX0pvYo zexCL3?XM=*o3&m&aBiFQPezi+TFn`;Xj=u)5Ylyng21^c12&{kj~+l4oE=rd;t$#G zVRu5MsIZQf4zQWsiG7}0L5;VkUB3;75Sl+B9rWUz3>tiglebu_k1`HXTY zzKrdq;0Xh-PPcWx5t;eF*{)ZSc_*-l;Fw}9#PySf?J~Jm8=2(f{RJX;9#GL1EQLm< zUBN8)6X$T?3WZC_#%FZ$j96hfMxh0x+=Bdg`})|v!Vxlx#ysjP_T6UrikR%F4ijr% zu?Uts%mBLS8%4Q);WQeJbJtJJnyXS>L=QR!8wOvy%v<|5i5MA=u`gjDYC)m!EP>l9 zH1Q8W{cbO(v>2JYm?1g7N#w|tvI4+CYB{K=K-xliWZz1?f3KYmV&ClIgJ2U_d?D;_ z;&eRON!(-jQbeKA180Fi!NV}V-6xL9{JNW2VwJ%nV4L9>bLvL&@Zz;Z*DIfD3 z7NE+oybC|k&v`1vK!5*bF_)>*2=X}yEH2ydMf|L(te(?`_9649l00Yq7Oh3!kn!-^ zM`BUw$-P0=L@r3UcxK1mgJaomIr4N!XgzcA z+7JrBW1U+HLF&||RvA-5S*!qcqk^38>8um+yuT;vef_rgoz)|g8;}+@m2vz+;QOW_ z2uw;BeWeQbZwbY3%~ii=H)w%6`AJCa6Gm@v;xVgqQGZ5uGzO(#|p0 z0j=WzB`#3dC1(6pZrItv#Ve8o@UQ1%Hfy2WqD0h08QDl0flBDw_g*-&%f(`|7| zP9Xz%;RbvsT4Y+ddxZCHrzT#q_*6U}0JIE1&bE%(+m;L4zVUkd6l4oH;iY9txWih| zXQmGf$-HpfJRV^t{>g|aIo(Q1dHawMvmZa(oZwOo{i){29a8>Q&!J7d{0ru2D$@5m zQn>1}+GNwxTINl(g(ete`s`bo#lc4-u5Gp3E$>o?O!7I6nLFlVE65lMeZVu@_Gv~X zL9!C*C!aHf*PA7w@B2T2BQ-hNzyi6#4y3Y?N9%7e#gYJWCpM?PK4k+OVp9uA#(CNI z%Ll2o`|N=yo^i$xv3=eNG8}c~6O01N2Z{w@o}^Rz92Ef$;*|mdE|Vy4^+w%1xgQB> zI(2URd)+q6q0M*jj^7Y}jkLk34?A7KPuK;-By)kAN6PwbZ_k^+iCO%;4%yikh9C>Zvg?Tx;wB7TJ#!Bxp809R4G-)M z3}z0W7RmtSMrSWFYM>SnVh0qBVNvIp;ELY&QoBdZPA$*_rv0n!IuKK+AIBWG*WZNA1!%`g&-p* zeDi}Pn~>C_(m}96mUZqyc1bn2>|rV4v#YwQ*~pkndd zLj(-or92KbRJDxwY-7)8yJIC4eT2Wz2@P}`cbEIMp*J_X`o4r1yJz@oW9*OfIbH7pax%rYhnWwwXA>2zTo5Z;N1pb! zVQ;9?Us`N$l)puOE}Nh9KC@N4n<8+q^Dln>0Kzy%TJu<@HMlwp)S9>|NEM3lvPAT++@*)p2J(3zNgc zr$a}!|6&{e`mzoY2B1=OMR1}56$=){{$1E&!*^4XBxa`-;rw8jF7|o1Mi}k8aTk`= za+(P^&kDC!B{?`J?^B!s zlj9pahHxxB-iPY}oOws8R7kPpsU^_g;w!G8%meYzl0K&oNw~0a4A*BTPx4^Wq~qeY zP-b7|R;|*dlVb=)fm#3KI(lF}yU>ew?A6vXGENna66lYH66l{C5X--ZWdtagG=}Au16xUhUM-G^gPjoJ^yG^Z z0r1y)L0FO_dFWXy7)kQ=xbPIinT8=TER8@^vo?agL6HDlmYhf0jgriOO~<)+lzpBe z(*!>3CGs3Lf;oV6X_FR-yDi%n7+?PX91pvmhW&aCQB*{qr$su1{e`(VktvzzEy zt(95g;a5ld!;bA9gSLB-;LFH<0M%B(>}^e@_FEL;HMH1 zbhh)BX*>4ecoFR{e~CL12v69p=tUl!gQe9)j ztsQyL>h~;ew91XH$pnM^c1L9g^VbCka(>)8bm~0`+xL}M{8Iyt>WOZ@Ki2T%CEycBGyw} zhf@mHVQO!IB`|5qXkXO?V0zYSrgPm1|A&z=9XiYXxu%G(9NNrGpR!Enq^XwrPz<{w z_>4=UjW5km!Ob1uTU`GjuI^8&6dT>ge}YVLb&31dB6_43k_{6rxii9NBvVFKyXAZdExfO*=D4817`t@}Rv=+u`(@|Es7`VCl`gh+?u z*$dqoLTJ5_)&^{`1++<)xH0bEww)nq>{b(!W)JG$v3%OH*((4lY*92-y)gMTg#T8_ z{^D_m>e03J!{_?1xmNsLDL%;L1#hRsA>0J#&2>4V?@O!GdltlyY)@2iux&;ilv=m) zdtn6qdzRe@@aURUH(U39>*~&?>Gk*MlC&_^%fD4+z*iMNEba!dAs<8FCS^|~30cJ_ z@Lkr%ydKhTt8BRJ31XrI#e_^U}Jay-_KTK19fCO8G7G?v_PvCZJgDF8Jz+W zUxpURrJR&o4<)B5eq;GoowoRf3sLEOFs5_Gi{$7qsy$A}pKTP;{@r&J_BuweIiizk zrWE#7{-{&j;);K>IHfIO4&({DdD9?3_*Jp4(CwZ~?spByP6f~g=&UhA(+B(N2w2fo ztQ(JW=z`rIsILO=3LvE7sN|_gFVufP`v>%Y!01AHVe%+qON&T~ii=1>7#lF@{}1U> zZou5fG1d?lkx*CFP|*+(7L!oX5R;Zt78g^Okd&5GmXMSZ6IEoE|Nlm8@q~0;ecgjS zm_^0K#R^D^xWNpoT9bC>3=@}8+bmb|Tn2{`;i7e(`EL3f?0#RW^$I@DE^`L3q;-=d zvH5P=sHHwB#itm6Cef^9@GpwvMl6zjh=xZuu1Y}rS*&?ZmC1wf&H8@#r)Cj60QB|%I<#C`D1S<^$v~v zjtR%#P61&JtUNs&91)!-2Vfy$ge*%~0X{(|RUT+C~)vt|BKuhQ^W7p%#-Q2z_jNWWW+wk(z%L3iok)bJ-P&gs0;o)h_VgYlttmhmoQfuwN=aYDbK#FbS z_Bu#)XJy`wD6SG?I}l*+l8lyL=P!aurST>Z(q(bf2=+dlI)r$)PL@4dSL3CO|6e+# zxQvE}#c_)un`hB(k!*Xcu!&2kKV{2s$m@7IfAar6nq8_Cf~XHSY?pB}wOe9vznBh- zsTTQ7qIlO%K2(TNlV~${!eAGW_TnbW662SeHlNgJ;nV5rmFdazMcv&Sh)^dcHAJEl zlhh@d1z(jarH@oH9(){i1Q}!fklR&@od4zwB+KJq{g1~_U`f+1?BX~%lKVeleu8`9 zN#){1er!vkc6t|?$-vwL<{9My9Czc}ODSi}k$*HbPN(7FJKZJfgACOiq@fd&4*cc{ z9&srDa3me{hN&94v@>?Am~_Wga-|z~rHt=4Z&DH^R$C?&;ThcZi6`c;;4ZF9QmN(| z;;bFG-zD%~CB5`d#{tjTvv6$k&bVJyr_n||Xj#&Wt|Mz*160)s!V>Xb-|F_Uk(}5L ztqtCr35YPGgJvygcx?Cylzg)Qy=apBkFYZC<=oM>ZUJhN6r^)KbJ3=b1?(t;$Xhf# zs+!6Tetb3GGgUm-5=+dyAqrV5|3I@zb3v1l)zm2+l9{mymih?q_nU5x9gL z56+lqUJxLi4Vu!$#^rP%lZV1}6S0fmd=e%;{ETLS^VY?Us_yqwZ$MEMOuS~^Hs^<^ z1reVEM^nNI4D0KNtOYTh1Dj8Z0F1J8ICK?N&XM{wMFB>AGaM_8;w+8xpAwK}m}l7~ zIrGH)*l61X?_Z#8CYbQVTw6u^)5^Ebj#lkNTzr=d0<;Xxkksx^oA1)vqyoB8rFJC@ zVge2}cw(-&L?Ris4s;T%Z5}W*8CD4*U$AJfCWg*Z+Pi6McTN&|k?0{LxlR*f1o(|mu zj0|RzclH(`J>8fLV3tq0HZKJ=U(nBpyz2}%6ndmG_?i3^h^McE;X3v?Dxl}UM|;qo z(z~`d{GAZvG5%5V)kwr{pTFH6S}=7F{#G)QtVg|Z6RQ?~Df!1puwzd+ko&)l0|p(s z2xS}vVv|1?x=rbKD$y(hB=%`SqY(Ft&596&NUS(2<33o^M3^whK@gsJ4@03EVYMLe z{aN*Yr~ki~U$6!oqc{*v4%a~J4^D_nig`x{rYUU@$?5JJ%Q-?kZDOTPMY38q@gH=Z z0lpVi=(TMhMd-z|4kDcyBXa4S@V%5|y=XUNu_pAKpINy{0!S%vRCJC>#xXN5tHRpC_5x8VX<(KkJ zZ~xd0k)oEgUV2gTL#)c0q!rU3>tD}xcf@+o{YnPBgQ<~k6h(T7{oW`_M$)lH=43Js zshZG?%|F^PF^yu{e7vQux|8GsAMf+FiO-zv|FSK4Uhnd$%`w;6+1Q9+I)}6|Pb|yz zY_mqWuge`Nni;$>(Du_*uvSQn@hMt=i`>3>2&c`qhRf7$m zQtB%X2^ZyS=qiK%NUH6ag3=m2*GL3RU@Ult;wi^e@6o5wFB63c&_r=&nO`RQ6QW7s z>@vSjgb|_1zr0~SOT;3u67iUR$CFq~pe@Qh^^PeqmY`7tZszPocI3ks+tVthEsR&0Z^#h`N}|9>|T&!W`=l8O!|4>cbQiV68o6%wj34I{_#0_nsTk>2QxmvM7wdscs zde?GX>ar|>r};WmT77ckRt6(KyClXdyS;s%OZ9jI6Wt{oOm`X#q@xjvQ}dI$q325W zED;O#V_k>Rz32X*SKe5vuF||{^$?bhn@w=%1M-*u!$}A^59BI7T}muipZMDxef+uU z5!u-RIj6H#(TAG4mQ>}cyJlx~WdXa*)#Qi&?j8OLY%tUu>@V+&NLg!>ARr|s$Q}$L z$R6f=I^@l{s^n=axbOG^XFmJ#&t zG8Fi|y>cw(#p}$GCUp)tH?Z;zzgq+=RZ-S7+tb;q4;CmgV1U2(S2Dz<)T*B!6ciC3^S3f@L%=xLnxfJWq(9+$`TCkVQJ!$w4zX>22HXfFtWVk!B)-qjEmBlssEPl4)55qi*4k`q-Z1=9X$90=NUzbLKxz?|;aYa? zb_DH6a8yOpzi!9E?^WAP|Ac>b`B@`OSqGQ*OjLFxwTmD-F5$0L0Dp4c!$!NibfB?L zfLdW#*HfczCJSo}jI68@COC^^4l-hy3&Hqp9~S*E8DS>aqaBHakCZEJUXim)#m%3+okHLIZR6-pIRo;R=I?|{adRa7?HiBU=+R-11^=lrD z(Z09kJYm+ssj^8{e)7p!ghzy!w@|pFmkn&%mSru+-WQPSSc>&ZbKfLXL0lx4`+RQv zuV+-l1w3ctap3Rsb*(x%GZ;8^t_9gj@6CAJ>;s3^_*>SUyU}%E_h4PmG8B<3DZV&}t`~qz_B&71bH$C?T2zzgfSMwfqw!O9h=m%PXg9}IPaWQvd>6+ETmYUqU7>#FlBXCcz zLB8?CWp zt1#i z)4p|9bTH12xcjBo%J;$035CJcIE+8W%vY*T=%{g-jIGp-74o#SN3+-L&%TsRVuYx*QiS~E`=WjU!LW{ zToXRMWck@&(j>e4t{nISYoy{`WLGs;)_p#;!on0g$ zIIdAFK?G@jX3&W>jVtC%8f|}GyP`;Gw(G7TwELG1$_T8@RZ-Fr)|syQc; zPf4Yj&k|8TaUX{Rru;N1KL_Sd@$!_Tdt3Z6ip!Kxt#D`{LvJMStP^GzWJw!mI=nxE za<@NXd=eR;eltVq{FQ^1U%wK!O-bpiq&`!Vg_DN0_s{}yn%GIXamgzKY8;Vm08%LA zT*VfUU~EyhFX6$&Ml)z0>I&AVH`N{QQ)Cvr z;WpIp;@)dG#HRhVEo;dV<%U)I}}(H(qpFE076 z_U=f%u6{N@N9$wSCvoWWGybF8hN4s#@J!D`WCpDhQgL*W=-Zr~K;B==zc)xEmLdXZ z(=d$?gde^Y+`og%mSD)#>!sn9;+9GphgoXx$H`hWy6_QC%a}erco#NEhO46@ zK?NiI&nzTH(<9V8cT7>tXD`;&yLTC{pnO`TSXZ&ZqF0<(L*fN0|}hifFEWP5Nf=C-(X)U;o22v z0$U@m_Ha?4d8YA}gvn8v=0-;~J0&Ap#B(z07e%=8mxsBX;nrO?UnbXZgL}IU-w1Ke%=}?eex)rrgCN)RkuCOu zGn9*>g?U99I)lf6r)%|t3dyzBHPn05v3UH-_}z~AeJ3~hfQ`$-sdNV*Y7mF}jqKFh zNrR(ZX)mtLZRHaIj*r0D9?h=7Ek7kLl%MgGWL#YKzJDmE-%k^fpin0`{&i{lV4`~X z1WMaQu#XPgV@@bX%3h*q8@{WUD}teDLACj4N(-=YIujiweT<`!lwc*mgNj{PRp-ea zqa3W^uS#pjHVm^l^l=Z6>IXxV5CQ);s?@U~U(Zi|1pjH35+k$xiDf^YTf4jk$gz|T zB6J>Fkuq2ANjpamA5eQw)%$ucGODxrQ0Q3t>05J+49M@#S(`$Z$@F36iLryMc6yjG zjN;j-KS(?tL9o;bjF)Q$L-ib<|J<2b4v5>W>Ir=vWihz}i*@9Fv6D;meZFR0HynJ(=-2;N+^RDY1??zXpezKN1gsBX zCdf$bU5rk+j3A^vTHZsJKQp$N*nL?W&apC>tA5CQx$I`pKCG6)7|e_Fa%zw4b+b0B z4nLCskLCE+01lV&9H6~US54nOojb=^bF4-FoNM0yA&K()*~%? zsxxkS>zyq+CH^N>9%}RbB(P&h-`*gqO#=EPp8NytDZi$hyK48 zq8(EmuVoNP_i5dFgY3u6Z{D|hH0T$4ZP@0s@dhm5w0>uH4$pim2NTs9=$b?$qv`ky zd!m6%3?H!!SZu$9m-_gSwg4h)PS4RKqofa^lag&YnnJz-lEy>uzbcOK;SU64`0#I& zWvcLPiX=Xt+u?vPSm7PHc>`)4^dx(s{Ow-@=`D2v`BS+23A_h1?9$lrIx3Rfn{k{e zLLiZ_D2lD!Dy_X_`{G9y(6Oj5$E+!DW)++_?XL3UVD9! zz`-O8%xxZ&kFzqqvDDJ8ItKN0Or(eaz7X!O1jHxyB$tg|J3vT+V2ncQ=4(EKuXFE{ zOUP`)nMka?IF%mK4hM~wbi{-3Tv17PS zi^<-OR%QARV{%SLg6E=uU2MB_N)5Hu2m(}a;k*4?2ZYOe| zt0YjNGjUxyd3oD< zed`($zoPrB;~p-30NccFeAm4PyQxBTW4vd=Q|uU6npOIZVWpX1O`yv~?S&0F3X`+? zJ0~kAN%I(#YSO>&ypr$VBP-w7D?5a;$@X@)HssGe zGceuxJCfz#YH(rUP#Wq(=<=I8LW<^M`?=d&D(a{@Q@}58vIX{qCLuhS9-f~h{=ry{ zE8=ATmq(MVlud1L5J27NLYNVstoH`Q{h}NMZ30OZ zyL^4r%P*fxFEtw0c^0x3AJV&kte28rOirmfu8i5NJ-8Ov>tUwI6=rI=pmRV!&PY;| zFM9elSY37ch%+%iPWQ-K$t}F|FA*b8kTr>2Ov$u(M_@_kBjLh7`>Yu6#FKO-Qe~vu zb|Y)BNHghPiecwKDUUc+|61YeUwy_azkuzKsuHov678SS8C}PxO$cqd$ZRRgq*0SR zA7uRV?W%kW`}0o-qUWOy^5A}Gqb*7UY|1vlt7CeEFW1J3;vH1=7-}^L_-wYZS(aSw zf5Gw$~Eiv^;#9ZcA_{a(X$hHL-+j0 zcW@ujE5$rMu$&Lw%|{1%s)lFfplWbDyxETOjo~!NquHIlZD74s*m5>xO7-iJ3*)9q z)s6JcO)jS#{9wP>mJyJXfg=EU>RSKPL;2uT*VJF}Bh8$zE!N{CX42h0q8AtmUS5<2 zZqLkrwYMOiUM1>gj=jvhbVcWf8YO<2BY5Vs{qZeB5$ncV=)i&mf*r9{H@~)Qc;yJq zi4S5s&s~HHF={<%5BJ@yAWCZ-V4FvABz(<=yFTjRinmn5lGlv`f?IN6^}QsK?{^&Q zM?YJs3hwKP8|_!&HSaN)wJkFHUpG_kBNr2v%WLp}o|vFPU1U<{R|{3Bg`PV-$Vhs` zg}!xOA$F-g(0mQ=9jmhRna*{6?>&7(p@|>86Misen_i%aL>G19 zboH!icBHii_#;oprec#@5}EAjA4cZ_EqB=Q@Wr!g@ribRq8~B@ZDn>IFh2{r>QHAl zt*Dj>o-#A!04UToH&d5ZwHgfn6uwfhq@Va>=u7KIAH11@g(tw}_c(EP^nb$mC(M7s zY7=({$jRXd35$qJi3n!~!vPHc*R)YgR?1Eevd6hmzNYBU?I^2b z#p|I|KTyH*X!LgENw%UM5jFKhn~AVU#(MHVl;=EVh#m7$9HuwPkhe_04D%3MYI&^% zQ;Cu{#FP2aOp@r$!%_Sc4}?yj&xu*P)N{39(~HXvzub=LTO6RCgbHPEn$dAJyqn@W z=KpZ4Z;CD0M~MK%9n8EyueJ0-F+xI%wV+!eXWqcKTzOHKXEI&5UVRp4;|z;f+9(-Q zLM=O~>WFS{D$6>n#?R#5WUyF+Gs3)B$)ct+zPza2bs5X>M3T$|gAm%3GSAag`}+y$ z@!KWpq)jgyk(|!ifg{}3UJXgWM4z8Gy1>8ZMB+pMm$rC$F^Ol5@v1qi5!ti(&|95q zTdLZ=00g=O>iz2;jJ6FU2$5+PlAx|%7J_-wj|m}X`u8c2S9+8hT>8fK-Khg)Gs>}N zyz&*D)C#Y2xK;5K-bym=aZOWLDK^>{K)4 zI%58*h1cE4y0Y5nEu3MF03LE<(|{3Cg<%4yl_M4mkDSYVIabN>gO((M7ehRU3&#j} zpd+`5p=jXs<%E9i{V7Q-FQE~z5*KPnTEV8PQkd|P@?Y`_9Fr`XpV-?L#$ZAkaW{a& z$e}xP&arm@p`!?tVW#R;G{w@CvBt=evBo}-vHmYa*p$q5F#+{VpkCE^EcW@ljy0m4p@XQk-=H3IIdrJgR^kY~E&W_>o)~AHC250%Ar{eOEdqUkKfErP7yjW) zEHCoSx>z215d6Gp-B>&fxcqnMX2bpPJFKLp^}Uv);e9MMVA_Df>fw|_lq_OWqDWI1v8WN>RFg8t%`R0f-LBup^zB~0D* zsywT)fH4H7xpMlKL>`?yGprTBo|)DPAaIcAr#d4JJ$-02b)>quo_+LrX3R-y#?~n0 zXgAWA7Q;%QL>0?NXh!pY3aQ}?j#4AOX*(=q3ZJ9+aLj;>4BLs`pn!rE; zY1Lb*0MEA8usG{<(q|@*{hD8@{rKu6X{>3{6dVmwTtauB>Kbx$XleN8WvW5O^i|1o z|M5Nx-0olWJG=#vQH#$klP6Wpqzk5#SI*&k;+ynUI$!8pj#XZxv8~mX{$4*lALEe7 zTxbI@K{wnyMUvOb=aaX~SCaRsQZ0%s*m8C=7Jy{hy&MqZ?0jruzNSk%biQbndK#J0 zZvr~|IDb>B7@~G~LU$6gYQsO(;~V$WnGzh@%6fz+*W-cujpwnKHhAXIrR}JXVrA>8 zuTf!=XgGF+aqIu#-~K#fO4M7XtS&!k2Nn+fvVooVYQGygfb*vJa?wNPE+6N$XH(|J zTL^lezvUnNE<#Zu0+S6o%bQth6J+)@&QAw_0_%vSGu|%jpp5_oj#qCe1kI~Y2|}23cL&|>YTLN6DYDM{inFM@HYABnyx;)!Cc*iRu*~@zMo1E~PWbTc z6oq!b3^a?Fz?PLSaMv$^WXCJM_HddaE`>1 zwT>fK%6Q;vem>E`;V6i4(qFsqJ(OwhoAgaqjf`8L3 z3x|&F33PehP3|!%|6UdAASTwfqmaK034KRG?LD<>leD>1U6@)mFwF;TOC1Yxy?fjO z%?wwSogN=|rQVF0ra2riT6v{+iyr6uF;{UFa+S4}z-nM9xmHc^>maZDP?_WrRpwnb zv2K>D@yg74>w`NFv2_GiXkDB zWVn@I&F$WYaa?W`mUiDi5;I?P0hmqLJt9dxV)^SSTTy`!{J`E<^MFn};-i?*dS+lR zO6;*IyPfE1vu))sdIH7z?SGbQKYw2*JMe!_UiNPIe*Sj8{t#a$XM9l!QDI3jd`?c4 I*Q)sc3;OW-nE(I) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index e78e1b112b..ff55281736 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -1000,30 +1000,30 @@ primitives = Map.fromList , prim "goal_apply" "Theorem -> ProofScript ()" (pureVal goal_apply) - Current + Experimental [ "Apply an introduction rule to the current goal. Depending on the" , "rule, this will result in zero or more new subgoals." ] , prim "goal_assume" "ProofScript Theorem" (pureVal goal_assume) - Current + Experimental [ "Convert the first hypothesis in the current proof goal into a" , "local Theorem." ] , prim "goal_insert" "Theorem -> ProofScript ()" (pureVal goal_insert) - Current + Experimental [ "Insert a Theorem as a new hypothesis in the current proof goal." ] , prim "goal_intro" "String -> ProofScript Term" (pureVal goal_intro) - Current + Experimental [ "Introduce a quantified variable in the current proof goal, returning" , "the variable as a Term." ] , prim "goal_when" "String -> ProofScript () -> ProofScript ()" (pureVal goal_when) - Current + Experimental [ "Run the given proof script only when the goal name contains" , "the given string." ] @@ -1188,7 +1188,7 @@ primitives = Map.fromList , prim "split_goal" "ProofScript ()" (pureVal split_goal) - Current + Experimental [ "Split a goal of the form 'Prelude.and prop1 prop2' into two separate" , "goals 'prop1' and 'prop2'." ]