From d4ad899b2effc0e1cb8adff42cc811383f2ec9cb Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 7 Jul 2021 13:11:39 +0200 Subject: [PATCH] first --- .gitignore | 1 + README.md | 6 ++++++ acsl.txt | 34 ++++++++++++++++++++++++++++++++++ qtuwu.png | Bin 0 -> 5615 bytes quox.ipkg | 12 ++++++++++++ src/Quox.idr | 4 ++++ 6 files changed, 57 insertions(+) create mode 100644 .gitignore create mode 100644 README.md create mode 100644 acsl.txt create mode 100644 qtuwu.png create mode 100644 quox.ipkg create mode 100644 src/Quox.idr diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..378eac2 --- /dev/null +++ b/.gitignore @@ -0,0 +1 @@ +build diff --git a/README.md b/README.md new file mode 100644 index 0000000..db91c2f --- /dev/null +++ b/README.md @@ -0,0 +1,6 @@ +# ![](qtuwu.png) quantitative observational extensional(ish) type theory + +hey what would happen if some idiot tried to weld qtt[^1] and xtt together? +let's find out together + +[^1]: actually grtt but wtf is a grox diff --git a/acsl.txt b/acsl.txt new file mode 100644 index 0000000..d82e332 --- /dev/null +++ b/acsl.txt @@ -0,0 +1,34 @@ +ANTI-CAPITALIST SOFTWARE LICENSE (v 1.4) + +Copyright © 2021 rhiannon morris + +This is anti-capitalist software, released for free use by individuals and +organizations that do not operate by capitalist principles. + +Permission is hereby granted, free of charge, to any person or organization +(the “User”) obtaining a copy of this software and associated documentation +files (the “Software”), to use, copy, modify, merge, distribute, and/or sell +copies of the Software, subject to the following conditions: + +1. The above copyright notice and this permission notice shall be included in + all copies or modified versions of the Software. + +2. The User is one of the following: + a. An individual person, laboring for themselves + b. A non-profit organization + c. An educational institution + d. An organization that seeks shared profit for all of its members, and + allows non-members to set the cost of their labor + +3. If the User is an organization with owners, then all owners are workers and + all workers are owners with equal equity and/or equal vote. + +4. If the User is an organization, then the User is not law enforcement or + military, or working for or under either. + +THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT EXPRESS OR IMPLIED WARRANTY OF ANY +KIND, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE +LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF +CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE +SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. diff --git a/qtuwu.png b/qtuwu.png new file mode 100644 index 0000000000000000000000000000000000000000..08a92e5218a60c4ee1b72168214449b5d3b811c6 GIT binary patch literal 5615 zcmVvPva00009a7bBm000hc z000hc0o46Tod5s;8FWQhbW?9;ba!ELWdL_~cP?peYja~^aAhuUa%Y?FJQ@H16?{oV zK~#90?VWji6;+nUf9Kw+w`C(CYyzUV+lT@RQ4qvNZ~+k!+TC^~@-=IQd)@kD1YEtkDL8Jy}8Qx$oClOcg?$$$-IZ9S}ks zHZ7|bg32OFH8OLxm$ce2b3|&)0mFa}9jPuNL$SwHDuqGmL?YEqa9N5nK%7d18Ubl2 zRyk70Tb(=`x`LSzRL1L0_4G=W^(3>HxM{;rG@<>XJ1*R_alI&D^vba|gTo();)AbCXVT zj-kwVTT95YwQJMTbnR71;ub-qGqbXw_A>BEBw{YPe!_$`P7Qy*pddRvHRTfty2Poj zQ;D!L|9#51E1!xt{Y&||8E2;ro}rU=n-Fxp0J#CcWNS&QL-IGS`-w;Bzlo)Q0a$E( z8nXEQ8?L;v)Q-`)xw+o{XPx<}BstcO{Hcn;);rgZ&AF|sbgvh@*JrSI&(%v`JW2TH5A+H^gl#H+-J1lQv2aj|S6dO^E*Z=3V?Y zD5WaHY}`LJXF}eJ&;K!O)s5?CYeLMD5LcmjkjjyMaQ)W~0S##R`_fUP@!2Pzv?d%m zYE&CRx76pmf%*7a_#2PG*1L^nfi_q0SYn}Y0BMe$;?^$Y>PM;kVb@kv?Ootb?{*EDcsk^lh9 zvd->pW4`TJ;N3Tk9sijC0G}@U^|nFE*|^SWPsB2w0-9R}CR4ALkR@*}#a*{Qg#Y>F zvoK9Z)0$38Or_RN%^Ck^pxGfB^==8-Qn&*dDGIxbcA;?d_TDt5$5BwV5rpn-`Cmj& za<7(gpPL!NTrAfx|(|m_2RWq}Gm~006=0 z-+N{O7hilnA_l>w1DiK(gWuoO`dwXJ1Ah5m3$fyZ71*_N2l7AuwD$~6A`A|M%*d?k zb0!p=cwTG%@~mF5s+ozCuEf%JSHMdqtVk1nxnLot&$te?HFa42K|aiIJ<_~DLx9jP zyTf^ErwxkvP{1%|-!Oi{=99mZudZE|)=$s)5ApEtArR;S>md+;#VC z94b4E{d@Por7?7kp%@5+2)f&cTjyMl88fFs%D5&Fo^n`96-U^3VrtHWyw1{5{`&P( zJero@S)!i8vMj9od^1Y+mm(AnBRxG0=bUpEF1_q~@OU~MN;qXPS?vm&)^A=dFaPV? zaSVym&!773gVhyPFAf_v1XoYY0a0=bOJ(J8L?RIk8FEI~iN7H*bHHR?X24uLZQS@z zx|aAF?JuwV^=GL*#;OQG2!RP#kBgbGqT(1{fAvlH8~wQb&RH0F>G!%+UbJg3e*M%! zu(B{?)(p&R@>B+{u&uc60~;=`IcMc^KNe))505nS^}TjL|O`C)yD;$rvD~jvReK9oU5L->kI%83RGZO zfD}N{m%C73-@fCuY2!AOmmPp60YQLQkKnn5FXDJrb%%&kbD|$XoG`HVK#+@4mAfJ~x9I2pfP90GkbXZqdsyjP|jo zlKrLlVCiyrn@5uaA%P#s3E>keV<@%|%jo z3T11;Tnlo`()`-7b8ehhxwkysr2}9K`%8}C>WMipO$&>D_X329R*7zziMRgczp?GW z0UT?nf?Ef^`l<|4x^TgT=K=s;dhrdEl@vqQ080UBeFow2e|-p=7GMA2Xs7|}YraB7 zs2&VJf-oj?7$mjr43-CLv8ApIiW%pm^lSHhvM^a8Xhq;R!>Ek}a6ID2(QpF}2WxRK zP=k`D0q(8`dM$ z3orx0h>o8;HVyb3-K<8Ob-1+zkm8!#>4yaDIpmN8cY05Vh3@bn!&#zU|E3O%v7{GpiCBAGp(k4wwQxy~|T$DZt z?vtFSlM8NgLnj>?>CK-SBs35a%0pFHQM)toE7vJ>Gi*9U0>FjSZY|9oobspsWNpFuDbpE z2&=YtnPNs*nW!@YI2fqGwz@+&60V0r><9COsRQ7VIt*oDYuzF2Z>ox!uFeRe#9xKV za3hX}8c-UjMz+=;=lRY;icE!9_}~_9Xrx1sY<=#eNgs;*2N70=o$D791`iy1>pj0M zdi(8!TN@Gpwl7;|=G-x3NdI#Ok1a1c45P6TQUXLkAWWEl?QQt}i1w2eFCKC>j?~s- z&yiB-%{Qi{0MnI@i4V^}Kv*~yZbVtI79~x`vCm(Lz5Ys+G*zK2Sc~dNQ?ip#<*WEIkd=`^6syI^Q?Mu6Z3o%$M4cYi;_hduw^^m3PhXV4_1Xr8!b zeA1otY6~R3Sij_hPZJeu^91CO_&0L%3|EThjEkm>!mQ8*kgDtEq$VYDCR_ofC;v`M zgn_Os+%jN%Le2o9)z)zDAZ%;wxC5FfMCfoeL1(nN+KcASs{!*I1_C+@3|8^4HWS>t zowG~Q&c+W0U6ZggS~$x$Fsb$^W?R)nyW4-^E%Vnw(d2Vg<`(IE{&2VBlOEjM|0+z) zz8spcKX^6Roeh!H-%EY$NX4A1x@gwCO_fV_tOPi&bszxXh5i)-djSp-BfvyWU~Ymy zBbfXEHxkItghnFrgSklv@|&SZ0I4zw{)v7DLI%(ohM1&e_7f&Bd*N67;X{w5{#Hw5x}a|F+gOYLM5lQMS#zaT*s4# zS&dI*WOuaL?~NPgOkH5dh?pz@UdDq400Te}KrMiS0JZ|a&YcHe@55<(C5ddiS+D|( z2Eb?zmJgsTR3JGH;S(B6i4e1lKKbO60!(q24gesCBsNjHX5`3WwHB-8c4S!rMk5e7 z`n59vpdV!=%RCV5g`i`WkVh|?buKf~5;B0$qYeQ8QyJAK$GJL!8Bh_x3`CDufq}mE zs{Ppc0Udtk3~59YTUHOnhb#+X^>3!EB@pk~ua-AY@P~YPr$5GUi%4VzJ8sBjLHe3b1uY zIDsHWCtGJK*=iiMgM_`-K?fC+ov~rIJ+N>r61U%nqbtbbgk%49DgNmAbitxqBAHrzn~!#hVE)RMT&$A{2`~6Fv*oB` zb_}qCVEIH(pA*f4GPZ`anr0=a2i!bu4t|3JeyGwsE`XCJKZP|7s zQDQrUM55j;vXgnDFf-|<_Pg#}JrUuEV;uzk!me!WDod$ES6*(kYd|9G+fwzYJC#OD z50Ip)z7^pD^mHKTa^AmHVB6DJV)oQoSRWF!C*#z?$`Z@$8W1nVg@-Qj>e|yMM%r7$ zB1ZI+trHG~uR|pSkN_Z}pCkbx0nz}WM~{}__ok*K1RR*Q+7*rIkb!qxzVX7+=#7DQkF;Gx!Uq(gdderJ#Ru|G6W&Eo73Hm*?)QxtHofi=(7Er!r#uI<~@u^-knF9Zcwd z|Jb7d9^jV>A32_(ovom}WKp0}*AI@EJHmN$q!aS??Q>rg=(E&C+I8KT&xw>LVX_>7 zKX)P@*XRyCc)0!~~e;9$^s-_}r^(3--NIpy|#-Z<{Y#HXrGn-r{y&Iaiz_5}`u z9rn_RX{l2?PMH$2Gymvtcf|EEfzAP7ezIuPg3xowL4wn9&BA-v^O#VO&C zFF&lfLO0yY3Dj=3pA`Ut0YFQM_M{!mh3k--NMkaptDTEx&fDhHmR_&2zWAtWy3U@0 zSk5>Rvk3@R0O8tbuRNJ-PsW^HR)2D?q?b!b(aPgL)-3HgBrvJWY>FPz18BbJr<3J{ zAuEC}8%ymg0Kh;15&3_Plr+;T4q;|dw6gkHO=Or+U}r^+K!060cV3MnCC&7>L)I?aowj>rO|H(`^~uty!qKA@iZ%j--W)*GPWU9W zM(-oaz}9-l-7Ce0dd{hm7JAenUu-%&)En^TsX+VJmL?T$jsVA+x<}2?UJcl8l_02` zwXGTWV9{;!+wV(glOA)(uEIm((sb`q;T8iU6nzf#3JkCb1k4BujXjQ4K~dZ#r-U|sA7cStaK2tV&SZLo04P_fF5f0>O%Wzi!%TK z6z%M}v(PJh+0~)}Us?&jlcp^U1<-#c$D*(45r+_?IM#X12YCC#=G!*x!C(<2V?o55!ktC(Y>LXSE{OU{(qF4@DSIHF>2K9B$*rOaO>!=97r5rzSr3;wSJa*!3!R*Q*`U`0X7K0e zWR-^I1-t{JajRs*V0>y7BI0lv3p2`v+x@E~nbnRSjb)uTdeE<%ROlh*j=RPr0Cy(f z>7U%m3p>?5lq=^0P{jQBGt=(vwnlreEG{qJS}`d_bH6Dey4?5A3P;xiTDBI5MXBU! zEHyucg0oj*FnGnHne(SRQql#z679Wc^q|$1k*bj)6?w0#K_Te|JlTMEKyy`=;4KtH z7#~|3lHrU7V&h>)O5&i`_r@#UdSrHrbT5)5<60!d3NVAwg_~{SS20jfSZ;lmj8+vu z^w7ea=e^`yQ5V^CcLwqB(T*J{=c<8ExTOAsfQWlP4`l&XusQM@#!1Zu#%i?%#g?sQ z8tqJ6IP-y|1w%XIlyFE3g@uQ+`)JzF+(Mr(AQD=Z&8m4vhETNR6o!ki$x2Gh?|1~_ z(&uOX=t$Q|opVY#q=jwU4)jSy$|G(eABwjsJCVZry;xo2yuZN!L(t4cGvl*=r4Uo(NfWPupY`@?+Q%X1&B?>cRAIV~O14rY3M#cO9v#Uoj%3qUxBnTCQekbu4b z(h%J)Nr1s14l<(&L{$VF1Naaz?PKC1GtAq6Klj11E^_QP{vZBLQdNdf1>pby002ov JPDHLkV1iUOqbL9X literal 0 HcmV?d00001 diff --git a/quox.ipkg b/quox.ipkg new file mode 100644 index 0000000..e9db42b --- /dev/null +++ b/quox.ipkg @@ -0,0 +1,12 @@ +package quox +version = 0 +license = "acsl" +authors = "rhiannon morris" +-- homepage = "..." +sourceloc = "https://git.rhiannon.website/rhi/quox" + +executable = quox +main = Quox +sourcedir = "src" + +depends = base diff --git a/src/Quox.idr b/src/Quox.idr new file mode 100644 index 0000000..39512b5 --- /dev/null +++ b/src/Quox.idr @@ -0,0 +1,4 @@ +module Quox + +main : IO Unit +main = putStrLn ":qtuwu:"