From 0b9251e22579aa3292ad64f00b5d0da2fa0ed369 Mon Sep 17 00:00:00 2001 From: Jeremy Bi Date: Thu, 25 Aug 2016 12:38:03 +0800 Subject: [PATCH] Add coq layer --- layers/+lang/coq/README.org | 106 +++++++++++++++++++++++++++++++ layers/+lang/coq/img/coq.png | Bin 0 -> 31207 bytes layers/+lang/coq/packages.el | 118 +++++++++++++++++++++++++++++++++++ 3 files changed, 224 insertions(+) create mode 100644 layers/+lang/coq/README.org create mode 100644 layers/+lang/coq/img/coq.png create mode 100644 layers/+lang/coq/packages.el diff --git a/layers/+lang/coq/README.org b/layers/+lang/coq/README.org new file mode 100644 index 000000000000..567d51b1fc99 --- /dev/null +++ b/layers/+lang/coq/README.org @@ -0,0 +1,106 @@ +#+TITLE: Coq layer + +[[file:img/coq.png]] + +* Table of Contents :TOC_4_gh:noexport: + - [[#description][Description]] + - [[#install][Install]] + - [[#layer][Layer]] + - [[#coq][Coq]] + - [[#key-bindings][Key bindings]] + - [[#laying-out-windows][Laying out windows]] + - [[#managing-prover-process][Managing prover process]] + - [[#prover-queries][Prover queries]] + - [[#moving-the-point][Moving the point]] + - [[#inserting][Inserting]] + - [[#faq][FAQ]] + - [[#there-are-empty-square-boxes-in-place-of-math-operators][There are empty square boxes in place of math operators]] + +* Description +This layer adds support for the [[https://coq.inria.fr/][Coq]] proof assistant (adapted from +[[https://github.com/tchajed/spacemacs-coq]]). + +* Install +** Layer +To use this configuration layer, add it to your =~/.spacemacs=. You will need to +add =coq= to the existing =dotspacemacs-configuration-layers= list in this file. + +** Coq +Official installers for MacOS and Windows are available from: +[[https://coq.inria.fr/download]]. + +Linux users can build from source or consult with their own package managers. + +* Key bindings +All Coq specific bindings are prefixed with the major-mode leader ~SPC m~. + +** Laying out windows + +| Key Binding | Description | +|-------------+-----------------------| +| ~ll~ | Re-layout windows | +| ~lc~ | Clear response buffer | +| ~lp~ | Show current proof | + +** Managing prover process + +| Key Binding | Description | +|-------------+-----------------------------------------------------------------| +| ~pc~ | Interrupt prover | +| ~px~ | Quit prover | +| ~pr~ | Retract buffer - rewinds and moves point to beginning of buffer | +| ~pb~ | Process buffer - processes and moves point to end of buffer | + +** Prover queries +The mnemonic for =a= is "ask". + +| Key Binding | Description | +|-------------+---------------------------------------------| +| ~af~ | Search (mnemonic: "find theorems") | +| ~ao~ | Show an outline of the current proof script | +| ~ap~ | Print | +| ~ac~ | Check | +| ~ab~ | About | +| ~aip~ | Print (showing implicits) | +| ~aic~ | Check (showing implicits) | +| ~aib~ | About (showing implicits) | +| ~anp~ | Print (showing all) | +| ~anc~ | Check (showing all) | +| ~anb~ | About (showing all) | + +** Moving the point + +| Key Binding | Description | +|-------------+---------------------------------| +| ~g.~ | Go to last processed command | +| ~ga~ | Go to start of command at point | +| ~ge~ | Go to end of command at point | +| ~gd~ | Go to definition at point | + +** Inserting + +| Key Binding | Description | +|-------------+-----------------------------------------------------------------| +| ~il~ | Extract lemma from current goal - exit with ~C-RET~ (not ~C-j~) | +| ~im~ | Insert =match= on a type | +| ~ie~ | Insert =End = | +| ~M-RET~ | Insert regular match branch | +| ~M-S-RET~ | Insert =match goal with= branch | + +Note the last two are regular =company-coq= bindings, left alone since they are +most useful in insert mode. The full =company-coq= tutorial showcasing all +available =company-coq= keybindings can be accessed at any time using =SPC SPC +company-coq-tutorial=. + +* FAQ +** There are empty square boxes in place of math operators +Math symbols present in your buffer (e.g. forall exists) will attempt to be +prettified, if you are seeing empty square boxes this means an appropriate math +symbol cannot be found in your font. You can either install a appropriate math +font, or disable the feature by adding the following snippet to the your +=dotspacemacs/user-config=. + +#+BEGIN_SRC emacs-lisp +(with-eval-after-load 'company-coq + (add-to-list 'company-coq-disabled-features 'prettify-symbols)) +#+END_SRC diff --git a/layers/+lang/coq/img/coq.png b/layers/+lang/coq/img/coq.png new file mode 100644 index 0000000000000000000000000000000000000000..36e4388bf1d5cc9c227c2bedfb6cac5d5e8affbc GIT binary patch literal 31207 zcmZ@<1y>tg*X5zmqQ!!{yA*ed1a}B7#T|+}6biHiD{dtehXA3tLveR^Ey0SretCbu zw<5DLvsTv3x##Y?&p!J`YpN??V~}AWAt7NaDavUhj@5|IAlh5RcL@s8DB^%(C#@!p zIG=#|WPytKO=G2~t%igYz=VYKB?1ZQ0deZfJ`$2Q4-(ShCnO}%3?wAt&p%tV#1R+X zTB<0>A-(?Z^{c%k8F2>vv!bCV5|Y5o|33d=(aQQFPQLR}QUku*L?eI8C&XBgc7}xH zH?Jfot?RdZ-0u6+WWj&^Ribg@ptjvA3|NH{hzHazlq=Ua=Bi<2k5+LWs3u_6wq$Ow zVs8j_-(FPTmOE+S7)mRZ7XY{GBgviqxseRsTW|jN^pdfJ`Vomik>fXqpJZ+qmyg}) z&%hJUiQoxi2r+CE+8GwYxCFZzmj7@oa?#_uK00P zL4Vn|G0pG7GcqzJDF&v#((v@~#70`!tFT&W5BmXt?yNQ(;QYc^Yw;v43RV}^4@D_y zDbq+^A5l|KdAWmTnI{m>-IeF#(6v2o_8Kacb@Qimr&r4CG5BV%dAqb@(&Ka1qo9(k1Eh21-pQUJW|V; zpo4FzrLC#Cy;It*lP zshG2A_;f$;@L6SPBbjl%fm%>#{+=!Sa+jMmc?%RvGUQ9}nfi6LWU?d<-#77oPKJWi@82@8U z)Y>6L#nZyYo0pXlqA5ka6UhBdgg+;X_B{eX2-33iQj;n^df-}{H0Qyx(%>K>U#am{ zsn;tXatnGU9|<-zTQJbW-w3{4v(IAc@9!Tqs!Tf%?&L-b&!a(`e=Gf46sw!ig2YE& zYZf1mvFJw>pj4(nT2con0Mb_)=&tBxnE#af`7tI0toLyTM5r^QD$eo)$@#FX(k;jmNTbf{ zYz!5QjEsgM@FDi{tEHw2hK?gxYt!q?WAn|jQ=Db>;+Fq9*~V?-9i(&a_W4?xqynvg zhdr_`f>w8KUeg6z0+!e3eU%Xcu4n=0V@7y@f0m5zF?t2ni?>k-yL{(OiMU3p+T9uz z6Xp|WGocJRY=LT!MOF9IjlSa?2@t1BpuV5{CaD{EF~sb@8TKyik;9C*iGzWPj4Z#s z-84HpoBT87ZB#(}i_gR@3_bi455p*$>As^$k0L1vDFL5NexEnLj&abe(DC?;zPefN zZcwE?BsV2#64M<{={N&gz3*p>Q!rh)`Y^+j`$6sUU7Cx;)betG$3{o+3-{{<_hs`$ zuxs0L9xe?%8YOk--j06op+B+RJT1%p_m9FY#nknxN76IAr*Q*2Vo_017nhfp7Y8M| zW+zkJ174l{W`pK535ZE4MLASMWt8@{$(@GY-rdlj3&=d^trK zWRZD`-+8z*F4pAvURvY_+44_^ERCgxXTp_+)6>JlEFTKyfUQX4w7{!$?DU9UQ&ZE$ zhBZSDz^iAa*<<09YyY$pZ?EWfX>mZmOdx7i>>$p0xug~@=eX&v!fcE;B0`6r-T-r5 z)tMkJ+kp;>n1PO&xj6y7GTmL6X=_^GT{?w|`gUF(Ex($|*x2~9PhaJeiKEN1^U@^P z(J4;Ig!a@)1|Ww`_qbI?4el?Vta_L&h6>NTZM>r@joJ-dJivPE3?xcHZDC@ zA_yuF1Oev@oyhja4LELWRvJ1}hpg2DAjJRHT78=}tcI!!8O)kJ7@^SjqvPW*vY${J zuiDyiBpgg=&+ujBlYZ?H%=h&1Jkk*j9-|=cP?s6HIoRTm!QFqnn0}n`95>%EZ&7s; z$=z|c?U6g2By9?PQ;7(G)j+(3@r}Yr{cy?55nn()w}0dx6)aj5==xb4x7=HEj6O{s zJ|dsiIG%{T`Bk%$?bVaHc4LZx>cW&{p>;nikxW%y0fG9}60a!(UVP?cB~dXkzCP{q zjduY}MJ`U{&?3&;`*smp6mT&=vZN6o7ng`rm!=mgpOZzsz~Hg&nq;H&9=T_;$uE}S z{imn4*5Jn*A^yzt*xodou-zz+=BE+8svOnI(VvM>KU5W*JpRE75==Z*)S}GW|13YO z$xdanduC&cwivtXH4)ybPh8H|*Vn6M7K>ym7v-C9HLjLiW&LJQ`MX^2wA2yYdND|! zuu6pQ(;Ju+$Ff4Gvt9EMEo>5K^+t`4QNVF=LW_j9N1itcqN_N-*DJb{qM%%MXnn2F z*5aE3_kZQiRDBWPd7c(O5JFC~W*oQX9UU91PXQO1qgUFijYQ4M)9hfRp~fAz%5Nv< zv&Kb~+IB=k%k3MY)*K5My|t>EmyF788vbC;`*?Z%d^*(c6wMs6-W?qs^~mimWTqEIgPX>DJHd!tr;LDhC@kguSRPy8TPX>jy8 zW_;x<&3EIp`iaRn<$5F2le`YPlo*LWh$uBbp0pAo5K)n^XVjqWz30EG&7dD~*p~U+ zO1GTt2G2e!&3Z4XL6WcE(p)P4GpMy4^GLX`ai3y$S5d+2v;1JnmKMUrUof{+&&kpc z+#uKgjit$%YG6mfI?2ZOH%?l@U}0*i`gL6F^rr{Kx8~;Nzf{}J1Hskr25oEQv}TRD z(nIye94X5{`o~*Bya2T>*O7(WSblczIr+|cD`MKE{qaj?^<=VW>XLG!exi`S%}5Pm&#Rj=t4OL(y`eW7`}_oja={xvbLz&j`tDtV)XSas zHyrA{!}2P#lf3^_K5kP#Pf>%c8FW~F?X&4yj=8D#wi48tu1WuTE0m&KG*M|#ZTY;v zzwd#AX@HCm_Yk2iilzOiRaMdLX3OxXUFYmlKs9&DlB(R9s9qxW`1pvJ2#+=KNBNX3 z9jBPAMbdo8brra9Khv&h>5l<6QCBUo+MZ6-oB)hhwnW8Vm7?jI_ec3Pi-jq79XOam zJ%5?hE-$Sa(4T)yVv_fzXzloxOall3*L7_x?0#doP@2{b!p`mN)WqS5GH5_eW8*Ei zex(s1l~hQOVZWCa1Ch)x2Qq&AS1vK>paEu)fN6Cp|j|RS>V0qfmNU7 zd0$som(+TTx6@~lfzMiat@HDGC(UrGq@mqw7`%gTo?t*VQ$ zhRt-=AwI;Z!zdP-3d&2RoUI=loJarig?z@UKn!_UMFFf>7KPgHKQ55O|_;5s^4k6axW&lWQw?^H^J2h7&NW<3}vw zKF=-_Q;5$0aewdcSWkusUtL2(k|G0I5AMcoqV{$RSD7x@Pdr4Lnx3()VG&^GL_xv* zixJkeZpMzlUBygYyYdg6+f^?ozMYSwtE;QCfByVo9P?{s!LKr?M&7v90?m0ij=w9S zUBM3?Vq9WSVvV*9lDvnsl9FM4&Jm~KQA-{lS4S`c2N##3%E~xZrmt}SSx15JU)3L6 zU0i@#T*uM{Pz)twcr!8cx$3p@`$6ExT7G_&0&%m$qz=`FhI+~E#|}@{F)#w?cXt^O zk3bTIH}6<4cGS_xG?nXYk86&Fg5vtoE@i7k(t~f%J)Z>$1yN2x4@t+YI7a9)Rkb;Y z$`+39Iy3~c`x?004n?W>ggyMy2x|YzCzGLnmw#8p?oU$nK46;W3K=?+nhMrrLLj8C zK^h}>YWE~?r5BukMjiUR5EGRrMIe$_0bgT8KYBa&<@))VVTUWs9RAmUp@<<-adK`h zGM~i{qEKznwuzRX^2vydT)&>K{J)UC0$!~=ag#z`BUk=#R)1{9;m9xJsSE{|GNs|8 zEktz{kW#&JDX9-1s_(VaUd+An5IjgcLF$I2*hZ;wuR{!9i*7x+N!T|PiCZ6@v(iu< zqDYShZNoPXr!lzFQ)K<1_O+qm29xR=Zg>m%*(^j!Mz$*xrp+BNi|PF{ldOJ-ZEgr- z+&L~FPkkQ+TP8+cZ8??jQMFWF_V_oynWIkOwy&3ucoJf8f+Rb4bL$x-i{$9SEJ(QZ z*yj|=lk2J7;ikv&iw>NE=9Gmf0-A%xs@=c)*+0;O>C_?OLswV)Eij#`g)%*-yN(10 zGru!Ns+r$jVbhKTPPODc=}9a<x#H_WlvZ`xrB#5Hb(b4gPe1rQNq(qN z_o6Abu&t1PtnOR)q?I0X;|FofvnHf`e?kN5OzOPVi;2q=m~v^)V{XIB3>iW1(^SN< z$%H_TJsrmruCK2p7N)1SsU(B^l%(vGtSk2R_V$mC=&2GC9w8fgW1uR1PEfTGx6C*c zaM7Ul?B&fOr{%TY*bE!l>iLEz^V@YzG@OPecY?mCu)h8}+|)$|?cyFI;e>)-F>8$H zW~9v=k0mOcXyHSxVD-50ISj=o5NmE0jg1O1hN;!OuH({gYZ5mqSkZv~BN>!gMO(X+ zZTSl@mf?cyfZ+Vr)<7jwSCzE;8lQhg%0=3osmjmXDgx9)r?~@}mF*2Nj3{APtN=5A zPeDFD*=CdC*4Aum-e{Xl7Ui#Z@jGqMt4Za)A}Tp}eL+!#;;>H4LHKX)OFn>Umm(>{ zyQDhvIVCvuTAi~qu%2I;IYw1VtZ#Ijbhv;q9I8=Eews}N&ig^8N`Q+cEC7Ed7j)Jn zTK%OG$v9&!;d4xqlaoUs=2J1bzAkB2HM?=5x29Ub-cgzzn1}nZUDwWAa6C%Da90G< zC4)vWu(dx`zykhcZ;v)phZg>2X~{60<_{0n^0E=$cB+&)&0=e4gkAjKDI-g}Yx?v* zADv?J#u@su5~zpMPYu^AIHr={RyUCN*kMV)2t@x&jb=+d=QS&PFY}9xO@_eDNXDsH z*&E76$6Ob*@oEMD78R{-a+ZDn%$07n*5ZxGpoDoxf!egHH8w*2@@wQvADh~+M&j+! z1x2MM*T7qU>VGpcI;yIwNn;I@D=RViENHYD+1UkVRfx=6avnkb+wj)nPfr5%-e-|N zin;BiDcT;FSw1g)|H>WIvQ*Pezyi6L9wGebE)3YmKG_BeSYy*?!&IqL_~Tx2gE2(c zU;UG9W?8es%`ZQf&T)>SMR;~T_z;!+ix4JkyS&^BWli=WOrFfZ(~8u zHtvrf6R|w`uAzpg`i8_vb$~liw_kbI))7~LstDzbjqWi1}An;0W<@!qbWx1H#jRJk{c~+cs9v!9w0ZxQAA(s^{X1bF# zW}2~A)=4O%$(D*xGCzVq0fB+UvZFF+UZ%{s+?y?2+RETQIt1fUF4FQ$pMXz!Q;zWB z$?yn>^el9=rn5@KCyI2MizM+R`YH~1=`}Db8i^jYB&Do<*=nwh4!TWq4Y`Z@50P6# z`GGG^94KIzB?ETFyg^SYvApg8yDn3?qLfT+oql_xpM-QNvJiY5F44n3`Y16$Uarfg z;&H4pZ%}}Mgy`t#0NzZFd8g~vr#~7?F4eXABLA6{#q*ici~OLg=lx2xprwmCH=B{k zF+(UsN;b+RIUR`$xbU|vE}6pqy1u^77f#j!v&v$cb0nO&{GN}t;LS=DqgxJ28e*ud zthCRPFVf!1`{r|Tm&j&heq*DO8iB<9odi-owLn(D>|{mG<|LY&LXo@Ge7H?Q&zgw8 z-rOAH^wxM#|0wqF&vah`A>+VlfSz9u4X;Qg;%&-(8l8Ag_vD2`sLdu&eWri5q3 zIe=G?y3^uI7BP>hBLlueu`+D?gOG{!&Y|G;hk{JQmWq?)EjkK}8|`e#QiEqlz~lrZU&#ZOx(_9Z8hl@LAEySrP1y zi?YZU5KNQjOa2z=Jv1O?)bxNt*N+}MS^=;I73J;bW)Vbu5!5lKQV(jX-t1GGH5oB= zd}}h%x>zZQnbq&>yubTK|MsFgnqo)9?p($RJ!k5G_p%45hhwYMs|En|HMk&jzdi

UOxl)^-r^GjcD|-| zHVl6jng1xx!V-FVxM$!2yJvGr9>1Nl9rS0_(Ek2{~HZ61f&^m6+eJ zE-uGLW)IJRU3C0wx84zzS`-WJcVvwCs6v9JkxD8euAyQ4GcAn-OgB!NNH8Y88L3Ya zg_urEOvQ_>c2eBpp+8D)Q%LX}M#GL#@jgkvry*EqwkVCGZg>Ady}T?d=!z8H?2+Sk zN(O%k)|pkmlviYkgbqZl^RJO+kEf`?4&9wwu=t(f8D-~rP7j7NIo4hs!zO)Va2;uW z7u!DFDVNHvvC?~l!fnkkWogvIc`F);yE!U?;xARhabz}e*^el*fYi4&y7Gv`;msUf zH>$t+YFX68btQ8gAGIz!JzY94Yec}rzOu6m4Y3jk7_tF?{~Slx298^7V{)I#E?|G2 z5ooWgTZ|#3z`XX6#@(EgV4Gv>lZn2+r)a(xzr3`OXFj5saMI;}>x+yK0K3cRJuf3nW_2C5{=9u>@-QAxh;Z7!1~i3)baSLj&bC_U*k{ z3A{V>w5lt@;{A~GywevYbz_pCOZ$7p3h?s_x438cW3JfH;rp*Ada2eXzl3bI#3y>( zO@10t4qTV&%I+!i80xWRJIsawsxd2ylJWI?dhf4RzAXy=0P3Ka;eOEZSmHC<%zHCK zk-@U&U(n-U&EFK2EF?3y-97^lJDl2xL_nP`UMDHma(qu0<+xDeON=n&0X6)gF z|8@Ij?kV?O{O8a4O-)1pRE-O*L}C_A@xsMrhOrj|MG{Eye5 zc1~P-cS_bm(kP1w?Nkoav|1C~osj*!Z>m#RU38y}L!-P+SwH@WJ|M{oFDhqniM#j6 zx$N`0&WM`NwQe}%`>^xp!#lCF-*R7yl)cn&N)omNtEA5}Qt0)*yU$N?!UJu7 zR7TfdOL+3ry^h#ra8tG&8+-}$y2YdNGf*vm;m5fAQu0p-E=VEjwZ9$j-~2Xr1df7_ z9i|Bg%VVqfr>yOT%m$nATeryH{EUFo2;88pq2$={h4HZ+Tg@)T{S5T4EXsKIc&P!3 zB4~+IGU~rS?#F#kpC5%|Kc7(yJ;V`u<%!Co{ii(B@b)H_P?*jY+^;qaDQcVS%rlz1Z03 zCIUbHM&${1GzKE0$HFP`)5a4v_y?VbZ2UR`4r{aVKI94V9$Yo48{nAxnqfxE)$2xJ zAUbjDUNdSB2;DujdZ68z!G}^`PTNsQWv2y1T1>w`)StoCB8UH819bN!J8&PJt^fHl zOVBcE7)~wOZ*aoj>TsSVAm|lyPo(~F6D7iRvh*t^nFy&IKHh(ca)x)8Gs?T_B{kyD zMU#r%hE3>KQRCINWrzf`g~nZE7oVK7o_=SLsc~x?>^P_E@dPnp2zU_UNX2H6kL`&u zVtF(8z0L(Y|C^YE@ZzDh(O4Jndju7C>rOeug3#nW1$?mKegpknl8ByU=*ys%n=F8NuqM9JvJ)r4#g6s8bU26n_U zyhj4iqTq$gjKNQ-rG{`^j%;N$qT(bRs3e7ZBqkEh(-R;F;NSxcQ>l0LWqO|Nnbrj; z_D>tGC0h4^a<05e25p_Obl#x|Fc+F7l+Fi1=e|JcSwRdIB)CJLrYM<_fOs+7AUqc6 zAKtlsY+M~B8(sVlaR#cg3ji!xX*4C=h*^qU%PAWl*zl}ZWONxX0Ux0Uvr0KDY9)e>8?0V>m0J)UoM)Rj9(HU#NTI{_{%< zF@97WNGu>Ve*^R8_jFw}A@G+2vZ>CbS7cMA#R}O$iZqi|(pXlVwKmpOBSAu0DcdYX zLS`lgy%kU$3r?ED!RK4}r6fFwm+T&wm4LGtLFDpMesVp}k#w^v%j4_$GTrZ1vL7fK z`bqZ=En&Q4Ru&HoqT-HS*F=emtl>(fxvUfM#8_a>7JfU4i6F5tZz@(KE*E~hM(R>d6`ryZK(6WX z{oEG5yN1X0M@-p;2HK+WJL|aTZ?-IH;^8z#KO;~BZ?w&O`P{&@QtVhZJe!o+)M2+XxudBX6CP*Vr$C z_A;iJ-1kNTK-Tl{wk}uUh)TNa|>a(f`PZ` zWkN#2ZnGu3>=s=p-|3X{_7k~BYkfoGt*1Zz;_lju<8)r0?EWV8I~u1w^i59>DkLZ% zVj!2=#lD#(B^T_2S zS6VcFWt+}sCI3tOyCUJWV(+yd2bpA#?{}B(w>cEziO$7`{(Q_bcBR-Xc6v}`!5HvS z*MbFPkS6zG(Pyp43Qf16e}#sb;Rn*9^+XD0twbRrMk;@h&Ng zKvq^3VSf6eUFN0VZ1Q3X0_k(jHkfuT39s#DWWhcN{5!kykZB$~eLd+vpFg zcK3<@X>IHAzH*LcJ@t~-%!#SPOaKA3e!FDf-1rE(E=LqY#m^^YR~tek4h*oy_z%cTqEG#GF;TA^BfZ4O zi(e#}E>Yjd#(93S{8|0%uPh${afxV*i`2M{QMvv0d$m%*&n zhcjBPn}m|``J4w!--b6+$o2abvb(4VaYx7M1d=YOj|WS2h9P-qa(P)9(KL#d3)f|f zghDAKgEHQT`FdD|a<9DAN5WMp{%*&M2Bck^k2-A;PQ|GAi1rd48yR8++!C2$uDlJ`vb(Y3r| zTmokCLENUa8r(UxKP~;N<1KZi zmoelU5?|YBlIt1D>%I)euwWCHz1OE#;iFb9naOQ`I4n08_B;F4wz%9fBWZi^+i{Lf zuga|QWU+cDG^6-lMQ9_4&(qU$_wt@^@b{0a^J#@+!>?j-ckqXoBBB0pwdRkbGj239 z{M8&W2IBGS0PQKSb}i(ppN?gpvY4R7c#*XAMsXg^s`W;F-V}#s1@<~RfE3iul2}c= zeQ-F8Z66FSE6d25rzwFE@TocX{1L>mEDkF>%E*d`m6d|S1C}$wfT2)L0DsRPFtcJ~ zW8$DSc_lvA{;=RMtbnJtYQde2@TW&+KqVO7A`DZ3nb=ypLJE>~u;6KiDxgr*kpTHXD_W!vxob-(@E+ED^l!}TcMfe@3LLPC1e>w8Aiv16(SC2Q^ zN;&bOP0e)XlP%NNP&Ya&a>M}(I4}X zv+MzBdZy_+wY5RVYrZuOV{Gy76E2F})&@Q`L>ddhm~B?}v!e1G?V(^8wAAry%CHP- z9j@I;(XL2P!`Lkb2sq>AHS_1U)nYV?o_M^gARxhvkjRLql+9K=o-`rZ)s6WqIB22B ztWp~>z5fI4M0p>v=nkv?y~LUrclYo~8yZ6H+d_sgX>A)7Jh9~!4Djp9iW!UD^Gp54 zVnp=srmN{@2N`#Uq%?|?UTgI#)sR$_H}@2{C=rRG)@;(xKPK?k?)g*ceOt&803_ zs9y&I?{GTL91gEV&7bye@6AImZCb3**PFdDm*gzn3C*3ms!9HeJ`YWDuz}|KJoUUO z)n=wt->3;qVzr-x7PPXAhD!)S4`3}HK>#ZM6aV*AV#5g?mt5g33hjCYX60IydPC_d zs(&wHCnop=bFFF&erZ;1fxismmZDQilv(wXXUomm#|nLZGu*@INFd;VVdX}bdFNK< zby#k;Rt^z%w{(~&h-Ng6PN0&&_^6>Vk(id2W?s5*wD8!`$(BA+ub`EZqMZfKuM>&C zgjKdnME@)QhSvR^2P4{gmZjb;3P`91)Z(vW%Hsz~D>t3?5tEwCO}M>WO#Dz{`Vd>p z2^Da|QgZ@CusM205~Bevxb!~>ro(%;2r3Q_83<~Lo86g!y_VnWK`I_&n>6N+FS0>* zrj4}@GxC!6R#KyrpQK)|LthC)Zx?skULTH@>H^Tz7P93)S^|W?IWnP2L^W}^eM&UQ zs?JACG}Q9t(wQqAYpldD&^73*bWoSjcK06$5cy1-# zMKd!oAr(trmuUnO;P&+NC|By~@T*xlIvyHLT)I*mpQx|axf3MD5(zQGWoJ!N6V%nW zFuNw6?-ZI(pkvreL;7vwaS>q+4SFwQ6CvQ-=i}3}uWNz#)nXgc9JXJDfnLBlO5rU~)mXSP2hQYTMjg5JzHWZSF}u)dE;Mv*_4#MH05kn5?ynu6 zke~q0m(v1NdOFrqw?9XbTMC(kQVz`vYXAFJxV)@b-;n6+HWVw;p|TuV-;?iAqd{Q!}1sbmR?j zd2A>G->AiJk+T=7Z0)Z#J%cc0gbq#)_HM{wbQak`r`62FYCVe8pU18ZA{4A6nuCI=T4n>ofy-^i<$;)OR+7MN6S>y{Jy*A=sCDFc<88T`A6!6PmBxx(%;$LsBn z>T2J8+m4E}?cE&wmr{kXkoTCF?#62;raNnL&F{*nyHst+ZF_*-@rEXi&uosc5#o+> zwQd^gYw&+pp1We~S;};oy+mjK1|SS+-#wq_RwfvVaM8wSR@S@J7F^*j3(iGGaW;yR5 z!BHm79^#p*A&gi(BMtcGdiXf+--8jhz%>}U`=hDQ>c>FAz?T?SlrVkxX5LrvI$v(7 zR~@Nt0ev?&=jk*{U~(LUYQfZ#Fe>lz*8G*pvst|S-9xnDykYO8S58Bkp7Oo;t>lC7 zN~23&XVvXbjBK#$hid$1!qbb52eR1EFtZ{zk$*l?1Q)I?xu&PdX!M*pumC=Oi z-i_~Q{6dSIU&yd7LhIUHr3idaWw|meZ6qejRT_EL+`lt>^t4%4GNjM;4WSs?2rzT8 zM^`oPks*9y@y5~lVy>MhMxw^X6DpRpDC*6l&l-}zPmWK+Qjh3KE;(^(EBM`$-VJVR zG71XhuUG$0t544?-nInVE0s)uQ8LqjZh>Ol$Ll>1dWGg47a@X#f$>0RAfNr|$zB>c zY-c>Xs;7aUD)RS(6Q5uZfU ztp?VEoexe6+G{bd1pr(uh=Ur*N1bYBb3RNaH{V6_(=k~}E?Z@UE?5_snpdiPBz z(&8+BrK(-;s;<7BBigQ{_^y8^!E>Ne=q${){f$N6mOurdN*EnFTzu`cR2M>-Abv@) z5qj*deNNI&Nofxa=!gDPWI9kRx!-%n*&g{$4r_m_CN{v&hQSifgT|_F%4YV3GA8ji z)_W?6e)@@jo6YTye&>@GZ8Qd}C~RO4X*^LikfFq+MtA&q&H$B_rB52++FGy6W4Ib2 zEy`cV)Di^n2m2D|teNf;PriGs*kQr&ycgdH-d1|z3F6Hj3mLg=+w@4ht08Jbr`*z%e;PVb_PI76_fC?YzTnu;9VhUX+S@a3R``b?_x3?~Q?{G|pT&MYW|)K6r>e}Drsk45-ew8Qute-#;W#t1Qs zez`VZ>=t4xgxl@OTKb+*&YN@>MubhzCL{zR$LsGxg5ta3zUJ-drZC{Ik4+jS{%~BI zBAbx=+MB?yiVkew6?j>4PFr#92pb>w>A0LM5Pw+pWU&0uvb>BaAXyo~`8vmGjrds^@sT!E8mrXreLl5H z;LVQEdSY{wCE#pO4~E41Y>&wwl~he?0TRFW-JRu}e(Hgy23>A_yD#W` zMLumgkcX|bWj5L5_<|a+C}(&|=Z@~KMR~zypvgBhXtMEf@&D~&n@Z(7Edy`2`~;eg zuP>45{Gy`{L^NT#q}e$IGJitv+Fzp+z%E%NQSo`?25CU19LvwY67oRo2d4*24Znw4 z3}i;+bu!e*=g(iC=c_LNJyLB>yd0k1ap%5@`)+s<_^$cAaaqFpS6TT~ixZmhdRp}w z75dov`ZYIT+kek{2{D>+h_zL}>UMUeAhZ0{ znmyoqyc?(?KBUv?>j}SJsI?g*a~^Rl%!T+s;^aaoxzW&`<;NQz*yw!`3~tA&pft;8 znkN=-qjUfL+bWE7Z!3Ma)bD*e`lubRCynO8_46BZ-s+w*S^#+_rl!+_l7mBgs}9Y* z-ZM1M8PBFvGBCBwS_x0O)oaIB@u$UP@$=QoT})uj0bs~_dln=3!w>u!{>3^A%G0K6 zB07d!$va$)lhsH%z;Z3=gQ(bns~a4FT`YR+s=FS-be1~}YHgP}zMn0z1D_ z#^;D%jn=mL?eh@SdZv`m^?i!NMPA`IY_9n9-Hs`nB3||bqVkx$mOj6IK&B2w& z(>PuQD(e_7tpRH)|AGE;ar-HCoS)Gv0`KRCySl1UNB-`6G%sxOR`q78z6GM`E0fN( zUv5+)XK(}ToyIN{I?vtq$xO!XOc2aoK_uW<*lLFWplm}YRmhlVUD}vHgXXv0HQ=`y zrqJ{N9cz2M$tI=PmnFIB^XJbhzW|3xN?ullhTX1uzYD!A3f+#m4bFXp1b|yz+ro|n zUAB{{?~pRDlQoAb(ZX06KVOM>21M(u1MPK02a1yXn z?GRAEvKY@-So>M0w7*L@Tew{v*;otY&f(-_K}=N6nlk>%1O76(pJ`rEUUWnC*@6hv z)_S>$F}GaXq&aQ5XPU=(Z<)yi#zm+A#BaxRN0G7^^@v5KzNx?0fz7R2i#{I{Xo%xs zVPl)B8<|SttFTs+Nk=%604>J6&2Nm<;TLs{w)@U*^f_ZcT%GK89=r#63eBo?SW-!I zv-X@ep5BLE)K^XOO%C+OyNVJh`ABtU!y&({VW9{kK0sW2899mJLZNA_&N zik*9$e|s^vK{=s8oBy2zUun6n)}*$&Hidno@(=GMd7|sQBERBkQApY*m1Ai}P=?QD=v+FYj=UrF7z>ZSD0+Q#DTLd#DCC&X5 z;2PhYNh&XI;s{fbIMWiKY&T5#Y;7IEgMl9YrCi9>xzHTS200bNzIhWj>vEKe8Z_lR3TrC0KkyHHb(jKTD`kZ;yEseJuC)R@;${@ z?4L53Oeu*>*G!KWt78lW=o&j>p8I&Cw?4f6pon_*F7&2RmC)&FmN~?^`pacL9x$V2 zoKwhbKtSKcV&dg%(2m#!JWL_?Q-}|w*(84AIYFxHGWg|s;`LI#Pq~(Oi2WW^n9}BX z%@lGujx&>^T7VXbHWc4+{nRaigWzge;Vx|UL%OW z{44H~*K-*{1v(-bQ_hM^HPZrwv(UxTA#ZekLS~oY$>#pNzpI4Rv*@&PgFbPIQ1mt# z;WGzK$03%qa%LD?X-;#VLc}H2D`Tn36-UPkGuY$)_eBvr4CWm8j%+@5?89K!)s~6% zplJJByyJ89j>kcQHu#$F%*;%CosFbcgiV%-?={GIqa`!+CYpLD+77bQ@r`P0$j*E- z;pKQj3lIh?WwDrDb?#^bB;ba3Ig_sqVJ%yBI-XfaPy?Gz9D-#5spBV90j(<{UKb3A zso;=8c_8|sXY)#UyZK6+2;Q+|tsqFS`DUZ_%pX7ec_4u=dE%QM$IU)s&yX_0)oaiq z((%zm4_^pV1`~{%dM^{k10G-6-~`kC49Gb@AU*WP;q-qIaGsiX)}v-`k$A55x6=~eCJ z4dnK?n#xZ3zL1XOf3G&>wYLxH5mcP`Xf|M=x=r@s7Y0~LI2}waTiA>f>P0`xq z@Uko>m#4#-q#wFa=hC>ZlGDaoWNox|kaa=+2ic?~6usx<|D_fU>c9Vb7Csh@kP>)} zS^OGoB!0VXbZmQ+LCn@&7=EZShy%5lM(WAtvOLF+$mH=_ph^5{RH3fS@kbD`AU2e9 z11#Y5z6n~;(WbiO{oKT*dF}(%Wk^ohP+1YTf2XFRl3+5^|JC)CL2Z0*+Z9@*6nA&0 zxDzPuu7v`{ix+n&l;Tp{p+JEqxVseB;x561TY!XO&;I`3-Vg6gW?+U{a(4IZo^xMz zS004vAq1$IApRL>yfDqDgVRHR8L)xhGESLA_B^}AcpdpuYxtrkfvdqb!&5X%R+2h`3O^n8$8X-qJ#qP=qhe_1lvf<8S!(}Az{>7*tYNp&~XmqT;x{bb^TohqG3 z>~$jILZ>25B_s2`dNNSyC&nv1oy5lB;{bP=deu~^C>v#4LyoS!Y*vo6;borX6{899 z@RY?yH8Tw%{JOfToQ4~>&t&~tBy_u@E~hA80vvOe0%+@1;hAMsovrmbl+WJXDX%Uq zMU_BwOmUjszuzw{G-NWS#rE%y*zBt^_+AZ{UL0P#D@38(n&}QR{N-xFSDOKdd;ibrn!aY5{tsM87GPs`%+M znL}IK;_VjI05j7B7PX2JTWXIi%@J(zp^U8(RzuJ+ZOX2zWpD$9q-tuTXl00HF9~mbAAkFIWRfcI!uMs~m+a)-{>*l2mN+LgV7Gk5YCN=Ik@uNPF5sfA(i3W{ZtqA=3?$WJITN#T& zQoUHete7v8+52q$1aWo6v5mro9~Jxv3+}wk4}uF}|0Rs3&KQT;`76!U;k=L$`fb4e z88Wi>7(}&pK^Kvb`)Rb~ZE2y4HeN!%;nc$D486h+bC2cidfYVAA0JEv6_pemfU0wO zD3Ezji!RE7#KRjgJvG(B0wR~w+J4={fmx*GKs}mQ%P#jrEFkCd^daDU z%^Sc+CRE;y@@l1o-}IJsm>hL#jJsBA`1j-{^hl#Y)Z=OnNcl~u1=ZZ8XX>pRBFsq@ zG2>8t*SN7z%!Pv;JyOmYY0c5E8XKmPRPp3+!G^KdYij{#sMy>fG4GN#VBG@=E6PuO zkZca;G;VaC(_5&udmu`RRyR=ar?2nG5&WLA8qnL|czC>n48+F2{j(*KQ<(wvAyWz~ z+(>1kKn}Wm>4oU6`mS(ti3OFlkoi^B7D_)8Sm;N9wum=igzsDQi!|RAfe(E|bKh|_ zfiOp9EdXLr)m>F9WpmqdJEn2<1;gapyu80?9m~fK>rY=V5_$4`_HOx*lgDh85MlB&!5v-jH_YH*sbMNMVax~eVu zqc<8bx;Yrrb`K#CWe%dzqt>8L0XE^c78j}uKT_UaBlj@Kl#~=ijoeFjghJ+s9k?Mwr~gvD?$>gCDUeIuQ~t20>~j z+BmPC>xd!FXJLIURE);=;3Uz~?cg|K zxi=OtSRP-KsY`~hv~Cx&pG&?fBGuf;cMU++_Y>j1{^QG+-}`+a5eJQSvC(P8 zZQ}Uy2XeAN#>3m&l4PLLttDqA_}Fk^rK@iy^)D~X(5i1My?-Fj5`urSjL2?<$1jWSOhl0+QjZ$ZYhea>r`g#(UJ1ibNN z764daH$EXSwh8Kn57xyijAVh~#it~e3S7Vb^p`gJX#X4QFY&p=D{0!WZg}88X{ntG z(`2@d6oEi1XD;?XX}QRh0U-e5zMy{E4*qyEY|{AEyN+)fS56Q6RMM-xOc(q^ooV9p zinXCWpYj4XYrKZq%<{Ujfh}qnt`9ED3w}k0t^4VTfGnA(O-cApFp?s-aeU%oxhjWG zx2^mKp3IETU4@YA(YVltFO?KdAtY|yCmNEc3`@cLP)>ieDZLQRhpl%V6;0Jih7)Ek zW3_87;U`u6**uT?l_a9F%o8jf2`m z!v)Xfr(4%3iC7`HcjQv<)dAXCh$K8O3M^>*|3gUL@klHa3M*AK+`VNusiqC^*O z&IR<)2=n1wO(QU*Dh(M7IBFqP*m7DK>^opxHjlhKN@hmq3T1+D+tgDPRy(EQeP^fb zjiI6N+uPf}EYb4m{%q+^E0uO+0L>TT^dUi)g1HI4QNUMQ&G6Hh$evHk9=cC*(MTlW zv634(#kN^4qkBP~u#!n8iznATKTdu-Onryj=(194SbEbsI4aIM>qXum6raS4!&7mg zywCChzd;h6lgM*o5b+Z8g-pYqI+i6$?-`G&*(t{(bmJiHZf(ZGZP6 zVDi`D);b9Bn}h^-{L1>kCk3Iz?fhFGQ0_~uSr$2?fnWKI-z$IKFipQok)3x5t-Utz&ONPW00AMTtWir^1*k)jdoatob(TOYQ z=RjCigVq`_J-h~Dil_gVzi2pyhD-^5x5L z$>$I0kiAncfT@qrP*oi&Dk`#dRM*vGOjG?)rO$dN(eyEx({Dt&uYQ2703#(OWZ7AW zs>Q|TGe(a#ZW>1Gi#Kokd!JQlzgLV}y5i0en27Ev*fbv)U?w@--g^iX@TN0z@YH%U=W&dbIyIK5MK=& z!c7X7@@Mlk)sWrr9mCA;bEhs>Ky$6GV!S~BTOU+&ajn*9!t2S!B&nMvAo)6RB3K%cX z*ItKM7mXgCFA_k5_R&LGL{%Q&Y^^u0d-srbkk0 z(jVCw-4(h+US8(R$#II1>Cb(g=5uWG<%WL(3cB}a>oYPkYc6+_80nRmY;;(NZs(IV zhBYIrfDPx9keJv}#mAN;0O;Xbs^_?K_wn<~3JH0xI>Vt0ne(0nRl$LM57~{$Oo$7q zs8n%J6P0hQuITuD+>u$}!tI;>?|%FQ-+_<>=)*Qh{Av;ZV~3N94BL@54Q6*)h;hiz z_!QikI(WeC`W=!h_>y?_X>sPt)9dnYwzJXkBSToXt4Zhi$(be>QHv$KME>YC>yqoe zFd!gY5iFOa_dnU)XnU6`9b#YeRflz31Pc%dv|x1}6~2*j5dZt$m|f=Nq`jgub zpU7StRG9R7k_++Xj$S~Yb|$JhViJOp4{>jY@hXRaVLU{{PeP#z#tx$`Ac|;d0y*IJ zrb|A+yY_B#xh}b$mYB&UmKg&@hnRd#&W~v5tq6E|_y)15g0r}wcQ3;u1{YUX2Itrf z@Kl(1_?<2W08F$Bgv5!!qTZ8PFzsmGvWG;2?L2m@XDTa=Z;IV+ z|8`>=RYBV`{iy>}BJu*`$s3&+N$Zr@F&dOp0S+pN-^6yiwSi<0FHr#vc;KF{6CP8l zg75Ci_s@#U>b7U2t5_6iGxGBGsvb9~Z*wK@Eip}CLO~}6$c?r$`Gxe)pdVV6z4}#x z`q0TicSlga7?w{=-`Y2#I3imE-Nw7VY$nU6@xyPQie9!D&7AbCxhP@E)DY z=bmT1!|4tC@-oplA1#XMMqOoTgsS+>VG}{AEqPv^^fEye>#V(ayEirBbd@kA@M-11 z;~(_l)aB`>QU<^xf%>R8vnYMTQ_A8ikX12#;PKZr=X7`}Gkd<$uz-M_@HBYu1772J z<6Ckxd#p7u3X<0B@f1OlnPaj0UXqh@i4k{BP%U|`O#kvYKKK5b_$lflO3A2})N$0p z!Y!#PVB1szA^DgB^J*W`cpOqd9#`Gt0ZY2W=bt9JEdeM6P(#lSG9*@~v1Nc;G-{qt z+S4_{Y*XWDZ}fPzCOtKi<7~M#^`uNcDSinsuD}P?tDUdO1gk#8!S4R!jGGaEP+Q!$ z<>#+&a-?)=QP!3?4l*9HBK$?eKJT+E98z&%C7j2>@?qaM6MeyU`7XmYPcz8AzQq4d zKKSX8@wVMPelv;kR&T5IsM6BS4Nq;R@$cX9z>7W3Y@te0!$0Xk=ig}TjJFIVFOm=c z{l#L^pkT&)@pu3(^}Xp+609^E9hAI$E^&V9J+(0Nz3?|N@xCU(J9t0P@ne&h7T1ZM%t*MYD*^uy`D>ilvnJ`_B@r)5;W7G& zPDs!h^Q9xtfusTNlWuVH;j(g>Kngabxg=NS?|gI&q|c z!#oa3h$2(+#X)9fFuw14@W(Z16?J|N$HK?-R1=fo;HTmIp5J<4A`Ee0FDAlDdUytl zA~s{lQ@&hpJKH(+Uj4hQ$6jNhzkQVz#b4#DPX^*Hv9qPVEx)q(K+WTTUZH6L-kxtPJE}*mfI3N$0`%Jcbz{*N*z{1OyZ)@{T!IoFan@PriNk&6Z z#a~ozx^aq#EMDa{nvO|}!1e5nn2)PZ81SCj3>PR(TQeHW44ed7(5@gsX+CC=(OEg zF<`;OyT%{k3_v6*K(3I_#+_uY8bhPAQNze8e{*P_>gy(>-SyJE!o%BD{`zQGJk>TZ zfT&C+oqoEyUEaJDhGPc(MIEq4Jsin!WoMG&)B)5g};V4ecD7IN055>nAv z;>pB0lcF7+xFli(IOw0xwF2H#RnhUu_mU==90l7y*oiVYQ+IW1Sb*2qS<9nnrEx=2 zK!IZC#}Zw4mNu+-*rt!fbvJV?U7?K{lyobgkoIc@S_m7;cl)^QnVI@VE93l>%2i)ULyN;Vj*@3AJVSXRvM{=FfH}9QXnbX@4Uf}cImL|C;-d)NgfU)8QBfG zz7B*!Nl^ZEd9S&ySN^s)nW<-$Ss+x?lOqWaB9YT0=tt}Q5?65qPFTOi zl0e=x;p>)-#l_+J0PfIN{_Y{|yh*aPQ(vtMMvRotL!Zf^NwY5T@%Gg9G7Agx47a&- zWOm*4Lg`Xfb40RBoBrWpuwXDN3?Nskg43r$d;fN{fmsPXWCp>lvt^!PpVV!nW6hduBz4BINyheX}ah4$a?hf4i?rwm2Xu$y~ zl^aknQmrFx$hI_3w5OsMUTU+H1mbLEPSGKk)+;isyd2V*xCB&nTaY7{y>CLRfR-a} zBI(VmD32Et*XI-o7L{Z8{t4A1XFFz3WeK%+{geT_s0lS-2f`IpR6CVYq7&=qBT=v-Ce9Om2|)_)29rR(i5l!tsPTQ zZo72BO>AQN!N4N)qvU8JTuKwGhx^5^5{Rdso;yG@9kfbVe9)&w3uWKy>jyAVLf~4p zRNhHVz}Kn2Z#I~4a(-JVH+EQWccsrAM!9y&{3ktCB<$H5!&{=Q?RgYCHeTcH82c?* zXS$a2g1%{eWW6_HNyIfpk6mqG0G62%W!Mo2@|xaStTYdL@_zgpM=k`A01uLvI+FKN z62N_sXuw|5LGWl>1PVank`3`+fLaYjqDy3EvM_ zYVR*>5F15Cu`ctTd<=fLE;nw9&%fU(MXq!`s{He7)e74%h6XGeqAF;J9xry3|(Wo-{7>$!9EcmG%`Rc3ynoDtT2P+-d7xQr&hTIY_TNd z3Xj|rG~CbnLwoVLI*01+u!m@(O9Dv5#D#1rGxAO+Q7Y0(jFm>|$P0wMDQ!m zwqHvCD+w_Quwf+7i~EW*`71>l?a#4XqjvMGPj6B)Yd*jA%8l*YUZfF8xWi3cT*ZnQ zZ>=_dVLwo*S3<%|SXwI~(mHw!coW!G!qQ2H*f)wnU;58po+G zwq?lcuc_Gv+>)6^{&LJ&1zIDiOTx{WKw$(#9PH3jZ+3^gyuY-4;#>IW&Pk0tSMXU` zS(j%@7J)UFmX!RydzY0a%07*wvS_tD(}yQ$ImnbjI-}H7tk}R*(<0&y z(L~cCl1>T3fkzjPeTHN?*x4;PWbMV2*u|ehySi>35ncH%fk(!pfh}f4E{1sd0G&i5 z?z+_n|Mu9%8W?LF)yD%6 z!AQ?4X0wr}E?rx zbs1#YR>vDC#*JaCUwYrd7^_o~I__@hQqis{rgWI&se{RU{^{iZOYynr zC*~Y<{V#;RI7Ji(3^AI~ZLl}e@93x)H|{c*xf<38(q8w51_tc$AQ%ORH}#5t5b} zkuW*6AP;*lmR0F`+07EP=7O^fU%K8m<<)-!y`LBQ0C*dpU{Ckdj~j?bA=Zi*5tpR= z`@TCQcK$6#rsGXH&&hH_Oz=ZlSFEM(=QBGHJ9eSImoV}kcit2vOSe{?{!+59qBZ3W zq1()>oak?qP5U3_z)(Tq{jmzRmm0^i;)l_#)gS z$_(Acc%`Swc1S!3XdAE{{5YKdU$~yceE~MR2IxU|zGAMSh919JFFiiQs})s@{6(NC z!0#5g|D-HH`-P%5_uJodU~o{x_Y&o4TjPm~vF@$pnz~`rZ46fczKqcAnC;`kmJJpe zc`Fo1+}!O>eCgQXx&5JIivdr~01(;0{!PyEO?jkR2}<#1|LkZ=b?fZ88sbne6_;9g zFBSx%k<{t-Jp7$z17wte10>AMD)Zb%Ll)E|E_UTbb4xT?7#tc7C57<+4fHrBs`_UU z9{nToKHClWzUq;;Uf}FuLXRnpF~e93CJLq5C^Kt`*xcj=&r5}Aa_c4kiiG#zV;8Pq z7?=gV{m*33{X7Wf9Taf}MFcM28Gk;q6Mqwnjks+x=NG=w{N}P2xHzJ8Sx!Z!Ziv1!$H9^ta?me7unyu?XylvO4_*iu zOW#vjbbT`;_+!ZCo97?Ej*D3HrmiuJeaw(D8}1dvLz?HdxaBE}{sAEZ-qI4xmw)Ir zyYDx{K|T+B+40MN3pVZw7=3zqzvRM4vu`UWR;}WF*akNKNlZK0VXD~P?=v*4T9r{F zd04IOT3`sbEl#Da>!Stt^9?CrTDr_~HZafR*?%SzTc>L&tggA!XkZ|AC(%`tnnEel zuh{xVeNS`XktKQW^7QT7-OZ#^BR6GA2AXmJ@|1e(;mn^a7(lk=Nx}gU<=HR&3RkOp znkbLK+hh-v&*9-`x3GW&<1#*93$k8b!wyfzaIlcdx9JWXgt>aUfU`HONwRpZHNN*~QcHf#HyCsYTEFH|gS5pe4 zTz&*Aq8aEQ-8O8-^US<)_oIrYTEA=iLY6}PvI~{2dzBOw>-N?JLZJz8IxWtAt9*yP zqzXjf{H4v{o?;`z=aUgZrz;)QDa^Mh7r+bBW&Pw|%S9SP&9<;lbdxfkN%DcBke||^ zYI(C#i{_ttV@-k7#ytI!a9c&Itv(&sfdsXXulV%L8M(Q;H4)VGrhwJj@4`B=@F2`N zwIxdA@>U$!fDL+@1f4)1$UGb58|iyz&oSBO5xK@i()?LM;Zl*Y4AP+MJeJs@`cfq; zytviJI?3_?CiC?tdK!>t5M$Q!4|vQidZV`%U>BuWV7CYwr7abl@RZF@Z(6m9Uv;>X~{ zT)|PRQKa(@5BsWuDJAYp1oul2R)P@}D;?suPoy=>?|qK*N!R(v)u1}$6^#TT^aZ?jQP zgTK-b#(z0q4Dws>(qUhCCdFZgANCwbjtVPe8PAuYOaAmJkn3Qcz^jJ|Qzj=`MVwHE zWs6V%*268Ue839P4z}w$77|<6{+|_HT_(Uqkp+{1xAfK`+w-SRZyib6RAdIN>j>8E zl0|QDxu6jjux`ta2yd52F;bb!8FCQA-8B`8x1qG?7FV zr^Lp`PXpQTCVUNPhSL&+BFS&zf2!_~*Yc9Wq)H|7HcB@5zzCwukg?b6O z0?4FGjYijJkkb3Sm--H^SApqv*=${-Brvkf*>sT8+XZ%UcJ}EhzNj8y)3O`Us8uE^ zel>1OA|WXCbcofsUi*5YN~c1f)nMd)d!Z`~wlFykXa5rsgcg|v`5i>_VqMus<-faC z*=nB+5)=(`Dr77nD+xN};iSQ&3!~#ElQ3XwVN+i+pG*70$3PN><8jr%DpnmD=62mpW#hX1C?Qh$#uEKo z7eZ-H;H+x3r3U}`Jfs`(@`YqKs~CYzj4DMw-CR~*ys@pKjv^~?{p#yUk+)j0+&yWb zvN&54)PwV7F&LS^cV&|0ZIcJz;?PGh^Qh)>r%)_`LSe6e@w$e6eJK_XU-UNp1cfVz z1bvF_c5(dsalz@zF^E)$4pU~;h*FNFH}D}a?^6CiuU6J)bVuEBskRu`9t)7jbl-VQ zXex-O2^T9ch5h6=u<#0?nh^x=mFd1A6z8HzjL+X)*Cu$iHp}u>qxP>xt!VuhcV_f$ zxJUVC>zy4mE&%+pEQ-iri{}-0&5?FWv*1+t*$O1}O*M7K-8>RRKQGoM9mnx_TOay0 zM8L$bad_+s6WaM?ENkE0GQ^6~te0?6q@%4@?{e&8K9~$-M2}5Oa3NC61lz6002M9? zDP=)hnSYthZ&ESWMxc|=79BxIZvBCBf3<r|>Lj{6b{vl_n$hxBA0N7nyv-7P=lSdT>nV}RctSpMT%qS3Wo;rx z;(xC0h0BD>d!jS@PWZbXmY@Ydy7tyRH(uO(BLeu0ZuHD7DF0cu8(0x6tN_yd0-_$Q z*qo)HXp%3`{3I-?T96gt<6|n6oszT_KnlhFrMYe)*2=Wb%WxBzZ{M(t7rt5I!xRq5 zz5Se)*oO!>4*PC?xQHH8Oa94Fbm=cLDi-N$T42W&O$Q9)<&j@hVdNyXi0`MA$A%6R)9wOFg<&&LieZG+^3g5i^WG7XXphg3?a^uI7wwk4~b}{MEQNnh(qw+=vis7U3!-w{| z7MN}^_P;X?FID{w(L&Ay#PP$yMdW1CXu5iT+yi@PWbJI?82QkFmE(6R<>kyPd8`EB z&nJOS+@1QqUAd;o{mr+@sac3=h=~f}j3q8HjXvi2Vpc0UYNb?`zVqeE&a7IQ{ z)dHQFDr@-CoR@9AF)xoKv>3GbuQ3<0W68`v>*+=HpcM#84@P<9H0BY#;OYanHtV6z z2r4y{2!A=J=|V(2HPkFC(8^MkhnX6;bRGO4*>3Ay$&yDO(_O0)S zbNeiKI7Y1;1Ink09w>ky*e3l!^~G87(w`9f(+V5qZsW+lIpqe<*dDbg$NO?+%cwrj zLmJ}4RU$)rwEJgrdcdv`iaqJ^ws@EgNbtlAF*4w`B+4pCw9}}A_`mH!M&%dhaV2JF z7BNX<6u;=V&vYve-4+?!v2_Izb6s7u7d2PP1a-=C*lqetNP&Jf(8mz_TKQ|kB)BAH z=LpI(lsI93?XvWv);UhTn!N(94$x7BB)o-;)_|!lDje_rATR1S?uC(}Y;vgF^RCt- zffMa7BkD!LZuH+@urls0;TaoLFy==39Dncle82z->~Q>i(3?w9pzray&6mDTsiM^ZHd)?GH;QLLqS{x|ZFvsVoKe7+-Y0BKKd$I>0AJD5MY!@T`vq)K9OWoP4}lgQx1-{t|@b zGEQYOVO?md23r-nuKo4HB!0O|$Lzefl{ zw8I9`0_s!_9kC_AoZi>h=caLIJ(!)Y|r4w{q6ANpPmSDAHv4X}9brhktV6aUc4qE*RMFw8mNQ zVf9;&VvpH9XHjgdV!?F6<>4;4ci`GVBwz;(A&KN}uzyRhEz)^}(pot^?V0uCrz6gI z)m^gyag)(tMGH_q#*#5KSTJ##d^q+I3b*FRkd=e);cc~FBc%CX@Ly-afF3&MEwH>d zcmM9v{Fl>TxftQS1X>u)tj(>J{EohGD+a+rQ}7DV@D7B(x6n12dV`)$nu1Re*&PZ6OP89-B|;V zr9Ax?H>3FT7TsWVc5z>Hvh3FGHzPc~;shFfP`Ay!SM6Y>oM9^*X<@~}h1qW(-WMCn z5y?D`S3P1fE6Cs8Lmyu*I6()_9tUgY3l^880>maiW$a zOm%g-xTcyg*y}*I1oH7qugRn6*lsbRHL(`G9M#cmTS^0#&PzB4L<5lA;pRV78T03L zAFAZB)n;K#rY4GlS2BmiqD^Z7_!Ue1oSB#tl20!XLEA^i&<&SlT#5Gi`AC4-V z(Kzos%Q(>EXcX2;joeG4ne|;#59`m z2TRG8K3Aoj%*BRhM*k@R>eAAg`!=)3bm4-X^q_6`0C*>=F#VD|+Mc@z6U?T@f~o4a zmm4k)8iWxQdg0z`-hO_H=*(_1a@{}h(aFCB{D*%Q7fBlIJu4YkF7s0rAHF5~%iAWL zNGMfYUM84H6+LeTAN8GtlTOdfsPQIlFiSr21nueM3-7*pjT0JBAPf3kba3dv`-h7F zk7ajc=tohSHI=qr>NiyEcL)zI^7UB;)9#&F1}T!iO-)TtolXNmo;N%9oq-xuR>%7c z&L_M4WGGs*$JrbxmD_G^Rw6j9DY^{X+e6mO$APZLV^#s7E1J{wklg#QB&xQ-a2(pg;&Yr@Y34$y(XAKKsUk z(tap);6(1KKlI!E3iO`By=B$zFcoixJBz*fBUy;vl<<9z8t!Xa09C{HSNKho^RmP) z$Qo#i_{TW6&jnnUpOU@Ta((i+eJOPMa(=%<*Y973&c;lt zoXLIj(E$rF!XOcGp_4I^G~j)NCEimn{{6w zpHF#bV({5vd|{r%Z_9{_^Bv)|GV(7k!in?ziCP6C(~Hn=?GE02G3i##2oBDWMD@Sp z3XxV+d>4eR*@fpk=m%(cZDXP?Ffp&%+aBGUMTEi0FM80f|EWxF9Ey zj{vR|C+luHMv5Nv?eV;qzg5-Ld_YsgW02;iuf%j~l&!iXS^uBt&?D$tw^2pB$H>6Y z5Sl8VyJEf}{Or#uBUSF_M7&{AkwKFYXRq!q>JpsWV$?_ftlv<1 z9je_MEe+UMtDMeywK>lirv;{XK!QK5+=x|m-i%l@v@(tEWG}6 z03k!eJ{e&j?-#dbIl=(5dH(Mp2*XawDdg@5@}AkFko6>D|+z zg~XJ5Lb22{fG9}rT>|w zofDyg0^bw?k=9H1cil2Xa??SP+yH1Zz%ckuYgm+a2aEB_R{209Wty;;Uyx&TnNYgg zttDXpk=eCt3v&N`cv#7bmvqf@b&4DF&Bt@q34{hZZBoiKb$M8WW`%wu#`hlG1-L0J zcAO+jzq%p}WMynL=sGvP#-yF8>wzBWiuSIBfcNVUte^Z*$`Dz`(Xb>l50j^L?pWn% zWx)wE;j^l$iqSG^Q_w!IIQJG)rv}j8PFWHy<-$?l<0G-b-kv505zsYGV9<5oo`xm- z;Y+By1O^RzF$uo36?#D#1R@v-S!WD$#8W;@nQkkw6TGy%JzdJI3pm)r+k?Td|KU;_ zy5c{@{LRUH{*$E>T2wJ_8p@MajTaT4TiaVuz)vha1O#PH4#xId0Bz5RVjiYk3_h-` ztW|!00Gb{%ddL}iSebiRi(0x_13#Yea`Omsatm|v3h8nSiVEji@} h|DOY#T&(PDeE +;; URL: https://github.com/syl20bnr/spacemacs +;; +;; This file is not part of GNU Emacs. +;; +;;; License: GPLv3 + +;;; Code: + +(setq coq-packages + '( + (company-coq :toggle (configuration-layer/package-usedp 'company)) + (proof-general :location (recipe + :fetcher github + :repo "ProofGeneral/PG" + :files ("*"))) + smartparens + vi-tilde-fringe + )) + +(defun coq/init-company-coq () + (use-package company-coq + :defer t + :init (add-hook 'coq-mode-hook #'company-coq-mode) + :config + (progn + (spacemacs/declare-prefix-for-mode + 'coq-mode + "mi" "coq/insert") + (spacemacs/set-leader-keys-for-major-mode 'coq-mode + "il" 'company-coq-lemma-from-goal + "im" 'company-coq-insert-match-construct + "ao" 'company-coq-occur + "gd" 'company-coq-jump-to-definition)))) + +(defun coq/init-proof-general () + (use-package proof-site + :mode ("\\.v\\'" . coq-mode) + :defer t + :init + (progn + (setq coq/proof-general-load-path (concat (spacemacs//get-package-directory 'proof-general) "generic")) + (add-to-list 'load-path coq/proof-general-load-path)) + :config + (progn + (spacemacs|diminish company-coq-mode) + (spacemacs|diminish holes-mode) + (spacemacs|diminish hs-minor-mode) + (spacemacs|diminish outline-minor-mode) + (spacemacs|diminish proof-active-buffer-fake-minor-mode) + (spacemacs|diminish yas-minor-mode " ⓨ" " y") + + (setq company-coq-disabled-features '(hello) + proof-three-window-mode-policy 'hybrid + proof-script-fly-past-comments t + proof-splash-seen t) + + (dolist (prefix '(("ml" . "pg/layout") + ("mp" . "pg/prover") + ("ma" . "pg/ask-prover") + ("mai" . "show-implicits") + ("man" . "show-all") ; n is for notation + ("mg" . "pg/goto"))) + (spacemacs/declare-prefix-for-mode + 'coq-mode + (car prefix) (cdr prefix))) + + ;; key bindings + (spacemacs/set-leader-keys-for-major-mode 'coq-mode + ;; Basic proof management + "]" 'proof-assert-next-command-interactive + "[" 'proof-undo-last-successful-command + "." 'proof-goto-point + ;; Layout + "ll" 'proof-layout-windows + "lc" 'pg-response-clear-displays + "lp" 'proof-prf + ;; Prover Interaction + "px" 'proof-shell-exit + "pc" 'proof-interrupt-process + "pr" 'proof-retract-buffer + "pb" 'proof-process-buffer + ;; Prover queries ('ask prover') + "af" 'proof-find-theorems + "ap" 'coq-Print + "ac" 'coq-Check + "ab" 'coq-About + "aip" 'coq-Print-with-implicits + "aic" 'coq-Check-show-implicits + "aib" 'coq-About-with-implicits + "anp" 'coq-Print-with-all + "anc" 'coq-Check-show-all + "anb" 'coq-About-with-all + ;; Moving the point (goto) + "g." 'proof-goto-end-of-locked + "ga" 'proof-goto-command-start + "ge" 'proof-goto-command-end + ;; Insertions + "ie" 'coq-end-Section)))) + +(defun coq/post-init-smartparens () + (spacemacs/add-to-hooks + (if dotspacemacs-smartparens-strict-mode + 'smartparens-strict-mode + 'smartparens-mode) + '(coq-mode-hook))) + +(defun coq/post-init-vi-tilde-fringe () + (spacemacs/add-to-hooks 'spacemacs/disable-vi-tilde-fringe + '(coq-response-mode-hook + coq-goals-mode-hook))) + + +;;; packages.el ends here