@@ -24,6 +24,7 @@
2424\RequirePackage{ifthen}
2525\RequirePackage{listings}
2626\RequirePackage{xspace}
27+\RequirePackage{textcomp}
2728%% ----------------------------------------------------------------- [ Options ]
2829\newboolean{literate}
2930\setboolean{literate}{false}
@@ -48,8 +49,9 @@
4849\lstdefinelanguage{idris}{%
4950 sensitive,%
5051%% ----------------------------------------------------------- [ Default Style ]
51− xleftmargin=\parindent,
52+ xleftmargin=1.5em,
5253 tabsize=2,
54+ upquote=true,
5355 basicstyle=\ttfamily,
5456 flexiblecolumns=false,
5557 commentstyle=\footnotesize\sffamily,
@@ -63,78 +65,9 @@
6365 total, trivial, try, using, where, with
6466},
6567%% ------------------------------------------------------- [ Prelude Functions ]
66−%% Generated using
67−%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'
6868 morekeywords={%
69− class, data, instance, record, dsl, postulate, default, assert_total,
69+ class, data, instance, record, dsl, postulate, default,
7070 lambda, variable, index_first, index_next
71− % trace, unsafePerformPrimIO, FInt, FChar, FByte, FShort, FLong,
72− % FBits8, FBits16, FBits32, FBits64, FBits8x16, FBits16x8,
73− % FBits32x4, FBits64x2, interpFTy, ForeignTy, mkForeignPrim,
74− % mkLazyForeignPrim, liftPrimIO, fork, unsafePerformIO, listens,
75− % censor, Writer, liftReaderT, asks, Reader, modify, gets, State,
76− % RWS, nGTSm, decideNatLTE, lte, vectInjective1, vectInjective2,
77− % run, myID, send, msgWaiting, recv, recvWithSender, create,
78− % sendToThread, checkMsgs, getMsg, viewB8x16, viewB16x8, viewB32x4,
79− % viewB64x2, pow, exp, log, pi, sin, cos, tan, asin, acos, atan,
80− % atan2, sinh, cosh, tanh, sqrt, floor, ceiling, count, countFrom,
81− % curry, uncurry, uniformB8x16, uniformB16x8, uniformB32x4,
82− % uniformB64x2, putStr, putStrLn, print, getLine, putChar, getChar,
83− % fopen, openFile, closeFile, fread, fwrite, feof, ferror, nullPtr,
84− % nullStr, validFile, while, readFile, userSuppliedName, seq, try,
85− % mkPair, getUName, unApply, mkApp, binderTy, divCeil, nextPow2,
86− % nextBytes, machineTy, bitsUsed, natToBits, getPad, pad8, pad16,
87− % pad32, pad64, shiftLeft, shiftRightLogical, shiftRightArithmetic,
88− % and, or, xor, plus, minus, times, sdiv, udiv, srem, urem, lt, lte,
89− % eq, gte, gt, complement, zeroExtend, intToBits, bitsToInt, bitAt,
90− % getBit, setBit, unsetBit, bitsToStr, findElem, replaceElem,
91− % replaceByElem, mapElem, anyNilAbsurd, anyElim, any, negAnyAll,
92− % notAllHere, notAllThere, all, length, index, weaken, take, toList,
93− % fromList, replicate, foldl, foldr, map, pad, zeroBoundIsEmpty,
94− % empty, insert, delete, contains, fromList, toList, applyKleisli,
95− % applyMor, applyEndo, absZ, negZ, negNat, minusNatZ, plusZ, subZ,
96− % multZ, fromInt, natPlusZPlus, natMultZMult, doubleNegElim,
97− % posInjective, negSInjective, posNotNeg, plusZeroLeftNeutralZ,
98− % plusZeroRightNeutralZ, plusCommutativeZ, modBin, modComp, div,
99− % rem, intToMod, modToStr, branch4, branch5, branch6, branch7,
100− % merge1, merge2, merge3, treeLookup, treeInsert, delType,
101− % treeDelete, treeToList, empty, lookup, insert, delete, fromList,
102− % toList, getWitness, getProof, FalseElim, replace, sym, trans,
103− % lazy, par, malloc, Not, id, the, const, fst, snd, flip, cong,
104− % boolElim, not, intToBool, boolOp, div, mod, strHead, strTail,
105− % strCons, strIndex, reverse, null, getArgs, getEnv, setEnv,
106− % unsetEnv, getEnvironment, exit, usleep, sequence, toHexDigit,
107− % b8ToString, b16ToString, b32ToString, b64ToString, tail, head,
108− % last, init, index, deleteAt, replaceAt, take, drop, fromList,
109− % replicate, zipWith, zip, unzip, concat, elemBy, elem, lookupBy,
110− % lookup, hasAnyBy, hasAny, find, findIndex, elemIndexBy, elemIndex,
111− % nubBy, nub, isPrefixOfBy, isPrefixOf, isSuffixOfBy, isSuffixOf,
112− % catMaybes, diag, range, isLeft, isRight, choose, either, lefts,
113− % rights, partitionEithers, fromEither, maybeToEither, strM, unpack,
114− % pack, span, break, split, ltrim, trim, words, lines, foldr1,
115− % unwords, length, realPart, imagPart, mkPolar, cis, magnitude,
116− % phase, conjugate, isNothing, isJust, maybe, fromMaybe, toMaybe,
117− % justInjective, lowerMaybe, raiseToMaybe, isNil, isCons, head,
118− % tail, last, init, take, drop, takeWhile, dropWhile, list, length,
119− % repeat, replicate, zipWith, zipWith3, zip, zip3, unzip, unzip3,
120− % mapMaybe, toList, reverse, intersperse, intercalate, elemBy, elem,
121− % lookupBy, lookup, hasAnyBy, hasAny, find, findIndex, findIndices,
122− % elemIndexBy, elemIndex, elemIndicesBy, elemIndices, filter, nubBy,
123− % nub, span, break, split, partition, isPrefixOfBy, isPrefixOf,
124− % isSuffixOfBy, isSuffixOf, sorted, mergeBy, merge, sort,
125− % maybeToList, listToMaybe, catMaybes, appendNilRightNeutral,
126− % appendAssociative, lengthAppend, mapPreservesLength,
127− % mapDistributesOverAppend, mapFusion, hasAnyByNilFalse,
128− % hasAnyNilFalse, fromIntegerNat, toIntegerNat, hyper, log2, gcd,
129− % liftA, liftA2, liftA3, guard, when, finToNat, finToInt, weaken,
130− % strengthen, last, natToFin, integerToFin, fromInteger, flatten,
131− % return, isUpper, isLower, isAlpha, isDigit, isAlphaNum, isSpace,
132− % isNL, toUpper, toLower, isHexDigit, isValidHeap, merge, insert,
133− % findMinimum, deleteMinimum, toList, fromList, sort, main, foldl,
134− % concat, concatMap, and, or, any, all, sum, product, Vars,
135− % getAction, setInfo, getInfo, lift, output, queryVars, postVars,
136− % cookieVars, queryVar, getOutput, getHeaders, flushHeaders, flush,
137− % getVars, getContent, getCgiEnv, runCGI, mult
13871 },
13972%% ---------------------------------------------------------------- [ Comments ]
14073 morecomment=[l]--,%
@@ -166,13 +99,9 @@
16699%% -------------------------------------------------- [ Default Listings Style ]
167100
168101\lstdefinestyle{default}{%
169− xleftmargin=\parindent,
170− tabsize=2,
171102 basicstyle=\ttfamily
172103}
173104\lstdefinestyle{numbers}{%
174− xleftmargin=\parindent,
175− tabsize=2,
176105 numbers=left,
177106 numbersep=10pt,
178107 numberstyle=\footnotesize\sffamily,
@@ -186,11 +115,9 @@
186115 {\ifthenelse{\boolean{literate}}{%
187116 \lstset{language=literateidris}}{%
188117 \lstset{language=idris}}
189− \ifthenelse{\boolean{numbers}}{%
190− \lstset{style=numbers, #1}}{%
191− \lstset{style=default, #1}}
192− }
193− {}
118+ \ifthenelse{\boolean{numbers}}{%
119+ \lstset{style=numbers, #1}}{%
120+ \lstset{style=default, #1}}}{}
194121%% ---------------------------------------------------------- [ Input Listings ]
195122%% Command to add externally defined Idris code to the document.
196123\newcommand{\inputIdrisListing}[2][]{%