<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta http-equiv="X-UA-Compatible" content="IE=edge">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="generator" content="Asciidoctor 2.0.23">
<meta name="author" content="Nikolaos Chatzikonstantinou">
<title>The rlean-search manual</title>
<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700">
<style>
/*! Asciidoctor default stylesheet | MIT License | https://asciidoctor.org */
/* Uncomment the following line when using as a custom stylesheet */
/* @import "https://fonts.googleapis.com/css?family=Open+Sans:300,300italic,400,400italic,600,600italic%7CNoto+Serif:400,400italic,700,700italic%7CDroid+Sans+Mono:400,700"; */
html{font-family:sans-serif;-webkit-text-size-adjust:100%}
a{background:none}
a:focus{outline:thin dotted}
a:active,a:hover{outline:0}
h1{font-size:2em;margin:.67em 0}
b,strong{font-weight:bold}
abbr{font-size:.9em}
abbr[title]{cursor:help;border-bottom:1px dotted #dddddf;text-decoration:none}
dfn{font-style:italic}
hr{height:0}
mark{background:#ff0;color:#000}
code,kbd,pre,samp{font-family:monospace;font-size:1em}
pre{white-space:pre-wrap}
q{quotes:"\201C" "\201D" "\2018" "\2019"}
small{font-size:80%}
sub,sup{font-size:75%;line-height:0;position:relative;vertical-align:baseline}
sup{top:-.5em}
sub{bottom:-.25em}
img{border:0}
svg:not(:root){overflow:hidden}
figure{margin:0}
audio,video{display:inline-block}
audio:not([controls]){display:none;height:0}
fieldset{border:1px solid silver;margin:0 2px;padding:.35em .625em .75em}
legend{border:0;padding:0}
button,input,select,textarea{font-family:inherit;font-size:100%;margin:0}
button,input{line-height:normal}
button,select{text-transform:none}
button,html input[type=button],input[type=reset],input[type=submit]{-webkit-appearance:button;cursor:pointer}
button[disabled],html input[disabled]{cursor:default}
input[type=checkbox],input[type=radio]{padding:0}
button::-moz-focus-inner,input::-moz-focus-inner{border:0;padding:0}
textarea{overflow:auto;vertical-align:top}
table{border-collapse:collapse;border-spacing:0}
*,::before,::after{box-sizing:border-box}
html,body{font-size:100%}
body{background:#fff;color:rgba(0,0,0,.8);padding:0;margin:0;font-family:"Noto Serif","DejaVu Serif",serif;line-height:1;position:relative;cursor:auto;-moz-tab-size:4;-o-tab-size:4;tab-size:4;word-wrap:anywhere;-moz-osx-font-smoothing:grayscale;-webkit-font-smoothing:antialiased}
a:hover{cursor:pointer}
img,object,embed{max-width:100%;height:auto}
object,embed{height:100%}
img{-ms-interpolation-mode:bicubic}
.left{float:left!important}
.right{float:right!important}
.text-left{text-align:left!important}
.text-right{text-align:right!important}
.text-center{text-align:center!important}
.text-justify{text-align:justify!important}
.hide{display:none}
img,object,svg{display:inline-block;vertical-align:middle}
textarea{height:auto;min-height:50px}
select{width:100%}
.subheader,.admonitionblock td.content>.title,.audioblock>.title,.exampleblock>.title,.imageblock>.title,.listingblock>.title,.literalblock>.title,.stemblock>.title,.openblock>.title,.paragraph>.title,.quoteblock>.title,table.tableblock>.title,.verseblock>.title,.videoblock>.title,.dlist>.title,.olist>.title,.ulist>.title,.qlist>.title,.hdlist>.title{line-height:1.45;color:#7a2518;font-weight:400;margin-top:0;margin-bottom:.25em}
div,dl,dt,dd,ul,ol,li,h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6,pre,form,p,blockquote,th,td{margin:0;padding:0}
a{color:#2156a5;text-decoration:underline;line-height:inherit}
a:hover,a:focus{color:#1d4b8f}
a img{border:0}
p{line-height:1.6;margin-bottom:1.25em;text-rendering:optimizeLegibility}
p aside{font-size:.875em;line-height:1.35;font-style:italic}
h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{font-family:"Open Sans","DejaVu Sans",sans-serif;font-weight:300;font-style:normal;color:#ba3925;text-rendering:optimizeLegibility;margin-top:1em;margin-bottom:.5em;line-height:1.0125em}
h1 small,h2 small,h3 small,#toctitle small,.sidebarblock>.content>.title small,h4 small,h5 small,h6 small{font-size:60%;color:#e99b8f;line-height:0}
h1{font-size:2.125em}
h2{font-size:1.6875em}
h3,#toctitle,.sidebarblock>.content>.title{font-size:1.375em}
h4,h5{font-size:1.125em}
h6{font-size:1em}
hr{border:solid #dddddf;border-width:1px 0 0;clear:both;margin:1.25em 0 1.1875em}
em,i{font-style:italic;line-height:inherit}
strong,b{font-weight:bold;line-height:inherit}
small{font-size:60%;line-height:inherit}
code{font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;font-weight:400;color:rgba(0,0,0,.9)}
ul,ol,dl{line-height:1.6;margin-bottom:1.25em;list-style-position:outside;font-family:inherit}
ul,ol{margin-left:1.5em}
ul li ul,ul li ol{margin-left:1.25em;margin-bottom:0}
ul.circle{list-style-type:circle}
ul.disc{list-style-type:disc}
ul.square{list-style-type:square}
ul.circle ul:not([class]),ul.disc ul:not([class]),ul.square ul:not([class]){list-style:inherit}
ol li ul,ol li ol{margin-left:1.25em;margin-bottom:0}
dl dt{margin-bottom:.3125em;font-weight:bold}
dl dd{margin-bottom:1.25em}
blockquote{margin:0 0 1.25em;padding:.5625em 1.25em 0 1.1875em;border-left:1px solid #ddd}
blockquote,blockquote p{line-height:1.6;color:rgba(0,0,0,.85)}
@media screen and (min-width:768px){h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{line-height:1.2}
h1{font-size:2.75em}
h2{font-size:2.3125em}
h3,#toctitle,.sidebarblock>.content>.title{font-size:1.6875em}
h4{font-size:1.4375em}}
table{background:#fff;margin-bottom:1.25em;border:1px solid #dedede;word-wrap:normal}
table thead,table tfoot{background:#f7f8f7}
table thead tr th,table thead tr td,table tfoot tr th,table tfoot tr td{padding:.5em .625em .625em;font-size:inherit;color:rgba(0,0,0,.8);text-align:left}
table tr th,table tr td{padding:.5625em .625em;font-size:inherit;color:rgba(0,0,0,.8)}
table tr.even,table tr.alt{background:#f8f8f7}
table thead tr th,table tfoot tr th,table tbody tr td,table tr td,table tfoot tr td{line-height:1.6}
h1,h2,h3,#toctitle,.sidebarblock>.content>.title,h4,h5,h6{line-height:1.2;word-spacing:-.05em}
h1 strong,h2 strong,h3 strong,#toctitle strong,.sidebarblock>.content>.title strong,h4 strong,h5 strong,h6 strong{font-weight:400}
.center{margin-left:auto;margin-right:auto}
.stretch{width:100%}
.clearfix::before,.clearfix::after,.float-group::before,.float-group::after{content:" ";display:table}
.clearfix::after,.float-group::after{clear:both}
:not(pre).nobreak{word-wrap:normal}
:not(pre).nowrap{white-space:nowrap}
:not(pre).pre-wrap{white-space:pre-wrap}
:not(pre):not([class^=L])>code{font-size:.9375em;font-style:normal!important;letter-spacing:0;padding:.1em .5ex;word-spacing:-.15em;background:#f7f7f8;border-radius:4px;line-height:1.45;text-rendering:optimizeSpeed}
pre{color:rgba(0,0,0,.9);font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;line-height:1.45;text-rendering:optimizeSpeed}
pre code,pre pre{color:inherit;font-size:inherit;line-height:inherit}
pre>code{display:block}
pre.nowrap,pre.nowrap pre{white-space:pre;word-wrap:normal}
em em{font-style:normal}
strong strong{font-weight:400}
.keyseq{color:rgba(51,51,51,.8)}
kbd{font-family:"Droid Sans Mono","DejaVu Sans Mono",monospace;display:inline-block;color:rgba(0,0,0,.8);font-size:.65em;line-height:1.45;background:#f7f7f7;border:1px solid #ccc;border-radius:3px;box-shadow:0 1px 0 rgba(0,0,0,.2),inset 0 0 0 .1em #fff;margin:0 .15em;padding:.2em .5em;vertical-align:middle;position:relative;top:-.1em;white-space:nowrap}
.keyseq kbd:first-child{margin-left:0}
.keyseq kbd:last-child{margin-right:0}
.menuseq,.menuref{color:#000}
.menuseq b:not(.caret),.menuref{font-weight:inherit}
.menuseq{word-spacing:-.02em}
.menuseq b.caret{font-size:1.25em;line-height:.8}
.menuseq i.caret{font-weight:bold;text-align:center;width:.45em}
b.button::before,b.button::after{position:relative;top:-1px;font-weight:400}
b.button::before{content:"[";padding:0 3px 0 2px}
b.button::after{content:"]";padding:0 2px 0 3px}
p a>code:hover{color:rgba(0,0,0,.9)}
#header,#content,#footnotes,#footer{width:100%;margin:0 auto;max-width:62.5em;*zoom:1;position:relative;padding-left:.9375em;padding-right:.9375em}
#header::before,#header::after,#content::before,#content::after,#footnotes::before,#footnotes::after,#footer::before,#footer::after{content:" ";display:table}
#header::after,#content::after,#footnotes::after,#footer::after{clear:both}
#content{margin-top:1.25em}
#content::before{content:none}
#header>h1:first-child{color:rgba(0,0,0,.85);margin-top:2.25rem;margin-bottom:0}
#header>h1:first-child+#toc{margin-top:8px;border-top:1px solid #dddddf}
#header>h1:only-child{border-bottom:1px solid #dddddf;padding-bottom:8px}
#header .details{border-bottom:1px solid #dddddf;line-height:1.45;padding-top:.25em;padding-bottom:.25em;padding-left:.25em;color:rgba(0,0,0,.6);display:flex;flex-flow:row wrap}
#header .details span:first-child{margin-left:-.125em}
#header .details span.email a{color:rgba(0,0,0,.85)}
#header .details br{display:none}
#header .details br+span::before{content:"\00a0\2013\00a0"}
#header .details br+span.author::before{content:"\00a0\22c5\00a0";color:rgba(0,0,0,.85)}
#header .details br+span#revremark::before{content:"\00a0|\00a0"}
#header #revnumber{text-transform:capitalize}
#header #revnumber::after{content:"\00a0"}
#content>h1:first-child:not([class]){color:rgba(0,0,0,.85);border-bottom:1px solid #dddddf;padding-bottom:8px;margin-top:0;padding-top:1rem;margin-bottom:1.25rem}
#toc{border-bottom:1px solid #e7e7e9;padding-bottom:.5em}
#toc>ul{margin-left:.125em}
#toc ul.sectlevel0>li>a{font-style:italic}
#toc ul.sectlevel0 ul.sectlevel1{margin:.5em 0}
#toc ul{font-family:"Open Sans","DejaVu Sans",sans-serif;list-style-type:none}
#toc li{line-height:1.3334;margin-top:.3334em}
#toc a{text-decoration:none}
#toc a:active{text-decoration:underline}
#toctitle{color:#7a2518;font-size:1.2em}
@media screen and (min-width:768px){#toctitle{font-size:1.375em}
body.toc2{padding-left:15em;padding-right:0}
body.toc2 #header>h1:nth-last-child(2){border-bottom:1px solid #dddddf;padding-bottom:8px}
#toc.toc2{margin-top:0!important;background:#f8f8f7;position:fixed;width:15em;left:0;top:0;border-right:1px solid #e7e7e9;border-top-width:0!important;border-bottom-width:0!important;z-index:1000;padding:1.25em 1em;height:100%;overflow:auto}
#toc.toc2 #toctitle{margin-top:0;margin-bottom:.8rem;font-size:1.2em}
#toc.toc2>ul{font-size:.9em;margin-bottom:0}
#toc.toc2 ul ul{margin-left:0;padding-left:1em}
#toc.toc2 ul.sectlevel0 ul.sectlevel1{padding-left:0;margin-top:.5em;margin-bottom:.5em}
body.toc2.toc-right{padding-left:0;padding-right:15em}
body.toc2.toc-right #toc.toc2{border-right-width:0;border-left:1px solid #e7e7e9;left:auto;right:0}}
@media screen and (min-width:1280px){body.toc2{padding-left:20em;padding-right:0}
#toc.toc2{width:20em}
#toc.toc2 #toctitle{font-size:1.375em}
#toc.toc2>ul{font-size:.95em}
#toc.toc2 ul ul{padding-left:1.25em}
body.toc2.toc-right{padding-left:0;padding-right:20em}}
#content #toc{border:1px solid #e0e0dc;margin-bottom:1.25em;padding:1.25em;background:#f8f8f7;border-radius:4px}
#content #toc>:first-child{margin-top:0}
#content #toc>:last-child{margin-bottom:0}
#footer{max-width:none;background:rgba(0,0,0,.8);padding:1.25em}
#footer-text{color:hsla(0,0%,100%,.8);line-height:1.44}
#content{margin-bottom:.625em}
.sect1{padding-bottom:.625em}
@media screen and (min-width:768px){#content{margin-bottom:1.25em}
.sect1{padding-bottom:1.25em}}
.sect1:last-child{padding-bottom:0}
.sect1+.sect1{border-top:1px solid #e7e7e9}
#content h1>a.anchor,h2>a.anchor,h3>a.anchor,#toctitle>a.anchor,.sidebarblock>.content>.title>a.anchor,h4>a.anchor,h5>a.anchor,h6>a.anchor{position:absolute;z-index:1001;width:1.5ex;margin-left:-1.5ex;display:block;text-decoration:none!important;visibility:hidden;text-align:center;font-weight:400}
#content h1>a.anchor::before,h2>a.anchor::before,h3>a.anchor::before,#toctitle>a.anchor::before,.sidebarblock>.content>.title>a.anchor::before,h4>a.anchor::before,h5>a.anchor::before,h6>a.anchor::before{content:"\00A7";font-size:.85em;display:block;padding-top:.1em}
#content h1:hover>a.anchor,#content h1>a.anchor:hover,h2:hover>a.anchor,h2>a.anchor:hover,h3:hover>a.anchor,#toctitle:hover>a.anchor,.sidebarblock>.content>.title:hover>a.anchor,h3>a.anchor:hover,#toctitle>a.anchor:hover,.sidebarblock>.content>.title>a.anchor:hover,h4:hover>a.anchor,h4>a.anchor:hover,h5:hover>a.anchor,h5>a.anchor:hover,h6:hover>a.anchor,h6>a.anchor:hover{visibility:visible}
#content h1>a.link,h2>a.link,h3>a.link,#toctitle>a.link,.sidebarblock>.content>.title>a.link,h4>a.link,h5>a.link,h6>a.link{color:#ba3925;text-decoration:none}
#content h1>a.link:hover,h2>a.link:hover,h3>a.link:hover,#toctitle>a.link:hover,.sidebarblock>.content>.title>a.link:hover,h4>a.link:hover,h5>a.link:hover,h6>a.link:hover{color:#a53221}
details,.audioblock,.imageblock,.literalblock,.listingblock,.stemblock,.videoblock{margin-bottom:1.25em}
details{margin-left:1.25rem}
details>summary{cursor:pointer;display:block;position:relative;line-height:1.6;margin-bottom:.625rem;outline:none;-webkit-tap-highlight-color:transparent}
details>summary::-webkit-details-marker{display:none}
details>summary::before{content:"";border:solid transparent;border-left:solid;border-width:.3em 0 .3em .5em;position:absolute;top:.5em;left:-1.25rem;transform:translateX(15%)}
details[open]>summary::before{border:solid transparent;border-top:solid;border-width:.5em .3em 0;transform:translateY(15%)}
details>summary::after{content:"";width:1.25rem;height:1em;position:absolute;top:.3em;left:-1.25rem}
.admonitionblock td.content>.title,.audioblock>.title,.exampleblock>.title,.imageblock>.title,.listingblock>.title,.literalblock>.title,.stemblock>.title,.openblock>.title,.paragraph>.title,.quoteblock>.title,table.tableblock>.title,.verseblock>.title,.videoblock>.title,.dlist>.title,.olist>.title,.ulist>.title,.qlist>.title,.hdlist>.title{text-rendering:optimizeLegibility;text-align:left;font-family:"Noto Serif","DejaVu Serif",serif;font-size:1rem;font-style:italic}
table.tableblock.fit-content>caption.title{white-space:nowrap;width:0}
.paragraph.lead>p,#preamble>.sectionbody>[class=paragraph]:first-of-type p{font-size:1.21875em;line-height:1.6;color:rgba(0,0,0,.85)}
.admonitionblock>table{border-collapse:separate;border:0;background:none;width:100%}
.admonitionblock>table td.icon{text-align:center;width:80px}
.admonitionblock>table td.icon img{max-width:none}
.admonitionblock>table td.icon .title{font-weight:bold;font-family:"Open Sans","DejaVu Sans",sans-serif;text-transform:uppercase}
.admonitionblock>table td.content{padding-left:1.125em;padding-right:1.25em;border-left:1px solid #dddddf;color:rgba(0,0,0,.6);word-wrap:anywhere}
.admonitionblock>table td.content>:last-child>:last-child{margin-bottom:0}
.exampleblock>.content{border:1px solid #e6e6e6;margin-bottom:1.25em;padding:1.25em;background:#fff;border-radius:4px}
.sidebarblock{border:1px solid #dbdbd6;margin-bottom:1.25em;padding:1.25em;background:#f3f3f2;border-radius:4px}
.sidebarblock>.content>.title{color:#7a2518;margin-top:0;text-align:center}
.exampleblock>.content>:first-child,.sidebarblock>.content>:first-child{margin-top:0}
.exampleblock>.content>:last-child,.exampleblock>.content>:last-child>:last-child,.exampleblock>.content .olist>ol>li:last-child>:last-child,.exampleblock>.content .ulist>ul>li:last-child>:last-child,.exampleblock>.content .qlist>ol>li:last-child>:last-child,.sidebarblock>.content>:last-child,.sidebarblock>.content>:last-child>:last-child,.sidebarblock>.content .olist>ol>li:last-child>:last-child,.sidebarblock>.content .ulist>ul>li:last-child>:last-child,.sidebarblock>.content .qlist>ol>li:last-child>:last-child{margin-bottom:0}
.literalblock pre,.listingblock>.content>pre{border-radius:4px;overflow-x:auto;padding:1em;font-size:.8125em}
@media screen and (min-width:768px){.literalblock pre,.listingblock>.content>pre{font-size:.90625em}}
@media screen and (min-width:1280px){.literalblock pre,.listingblock>.content>pre{font-size:1em}}
.literalblock pre,.listingblock>.content>pre:not(.highlight),.listingblock>.content>pre[class=highlight],.listingblock>.content>pre[class^="highlight "]{background:#f7f7f8}
.literalblock.output pre{color:#f7f7f8;background:rgba(0,0,0,.9)}
.listingblock>.content{position:relative}
.listingblock code[data-lang]::before{display:none;content:attr(data-lang);position:absolute;font-size:.75em;top:.425rem;right:.5rem;line-height:1;text-transform:uppercase;color:inherit;opacity:.5}
.listingblock:hover code[data-lang]::before{display:block}
.listingblock.terminal pre .command::before{content:attr(data-prompt);padding-right:.5em;color:inherit;opacity:.5}
.listingblock.terminal pre .command:not([data-prompt])::before{content:"$"}
.listingblock pre.highlightjs{padding:0}
.listingblock pre.highlightjs>code{padding:1em;border-radius:4px}
.listingblock pre.prettyprint{border-width:0}
.prettyprint{background:#f7f7f8}
pre.prettyprint .linenums{line-height:1.45;margin-left:2em}
pre.prettyprint li{background:none;list-style-type:inherit;padding-left:0}
pre.prettyprint li code[data-lang]::before{opacity:1}
pre.prettyprint li:not(:first-child) code[data-lang]::before{display:none}
table.linenotable{border-collapse:separate;border:0;margin-bottom:0;background:none}
table.linenotable td[class]{color:inherit;vertical-align:top;padding:0;line-height:inherit;white-space:normal}
table.linenotable td.code{padding-left:.75em}
table.linenotable td.linenos,pre.pygments .linenos{border-right:1px solid;opacity:.35;padding-right:.5em;-webkit-user-select:none;-moz-user-select:none;-ms-user-select:none;user-select:none}
pre.pygments span.linenos{display:inline-block;margin-right:.75em}
.quoteblock{margin:0 1em 1.25em 1.5em;display:table}
.quoteblock:not(.excerpt)>.title{margin-left:-1.5em;margin-bottom:.75em}
.quoteblock blockquote,.quoteblock p{color:rgba(0,0,0,.85);font-size:1.15rem;line-height:1.75;word-spacing:.1em;letter-spacing:0;font-style:italic;text-align:justify}
.quoteblock blockquote{margin:0;padding:0;border:0}
.quoteblock blockquote::before{content:"\201c";float:left;font-size:2.75em;font-weight:bold;line-height:.6em;margin-left:-.6em;color:#7a2518;text-shadow:0 1px 2px rgba(0,0,0,.1)}
.quoteblock blockquote>.paragraph:last-child p{margin-bottom:0}
.quoteblock .attribution{margin-top:.75em;margin-right:.5ex;text-align:right}
.verseblock{margin:0 1em 1.25em}
.verseblock pre{font-family:"Open Sans","DejaVu Sans",sans-serif;font-size:1.15rem;color:rgba(0,0,0,.85);font-weight:300;text-rendering:optimizeLegibility}
.verseblock pre strong{font-weight:400}
.verseblock .attribution{margin-top:1.25rem;margin-left:.5ex}
.quoteblock .attribution,.verseblock .attribution{font-size:.9375em;line-height:1.45;font-style:italic}
.quoteblock .attribution br,.verseblock .attribution br{display:none}
.quoteblock .attribution cite,.verseblock .attribution cite{display:block;letter-spacing:-.025em;color:rgba(0,0,0,.6)}
.quoteblock.abstract blockquote::before,.quoteblock.excerpt blockquote::before,.quoteblock .quoteblock blockquote::before{display:none}
.quoteblock.abstract blockquote,.quoteblock.abstract p,.quoteblock.excerpt blockquote,.quoteblock.excerpt p,.quoteblock .quoteblock blockquote,.quoteblock .quoteblock p{line-height:1.6;word-spacing:0}
.quoteblock.abstract{margin:0 1em 1.25em;display:block}
.quoteblock.abstract>.title{margin:0 0 .375em;font-size:1.15em;text-align:center}
.quoteblock.excerpt>blockquote,.quoteblock .quoteblock{padding:0 0 .25em 1em;border-left:.25em solid #dddddf}
.quoteblock.excerpt,.quoteblock .quoteblock{margin-left:0}
.quoteblock.excerpt blockquote,.quoteblock.excerpt p,.quoteblock .quoteblock blockquote,.quoteblock .quoteblock p{color:inherit;font-size:1.0625rem}
.quoteblock.excerpt .attribution,.quoteblock .quoteblock .attribution{color:inherit;font-size:.85rem;text-align:left;margin-right:0}
p.tableblock:last-child{margin-bottom:0}
td.tableblock>.content{margin-bottom:1.25em;word-wrap:anywhere}
td.tableblock>.content>:last-child{margin-bottom:-1.25em}
table.tableblock,th.tableblock,td.tableblock{border:0 solid #dedede}
table.grid-all>*>tr>*{border-width:1px}
table.grid-cols>*>tr>*{border-width:0 1px}
table.grid-rows>*>tr>*{border-width:1px 0}
table.frame-all{border-width:1px}
table.frame-ends{border-width:1px 0}
table.frame-sides{border-width:0 1px}
table.frame-none>colgroup+*>:first-child>*,table.frame-sides>colgroup+*>:first-child>*{border-top-width:0}
table.frame-none>:last-child>:last-child>*,table.frame-sides>:last-child>:last-child>*{border-bottom-width:0}
table.frame-none>*>tr>:first-child,table.frame-ends>*>tr>:first-child{border-left-width:0}
table.frame-none>*>tr>:last-child,table.frame-ends>*>tr>:last-child{border-right-width:0}
table.stripes-all>*>tr,table.stripes-odd>*>tr:nth-of-type(odd),table.stripes-even>*>tr:nth-of-type(even),table.stripes-hover>*>tr:hover{background:#f8f8f7}
th.halign-left,td.halign-left{text-align:left}
th.halign-right,td.halign-right{text-align:right}
th.halign-center,td.halign-center{text-align:center}
th.valign-top,td.valign-top{vertical-align:top}
th.valign-bottom,td.valign-bottom{vertical-align:bottom}
th.valign-middle,td.valign-middle{vertical-align:middle}
table thead th,table tfoot th{font-weight:bold}
tbody tr th{background:#f7f8f7}
tbody tr th,tbody tr th p,tfoot tr th,tfoot tr th p{color:rgba(0,0,0,.8);font-weight:bold}
p.tableblock>code:only-child{background:none;padding:0}
p.tableblock{font-size:1em}
ol{margin-left:1.75em}
ul li ol{margin-left:1.5em}
dl dd{margin-left:1.125em}
dl dd:last-child,dl dd:last-child>:last-child{margin-bottom:0}
li p,ul dd,ol dd,.olist .olist,.ulist .ulist,.ulist .olist,.olist .ulist{margin-bottom:.625em}
ul.checklist,ul.none,ol.none,ul.no-bullet,ol.no-bullet,ol.unnumbered,ul.unstyled,ol.unstyled{list-style-type:none}
ul.no-bullet,ol.no-bullet,ol.unnumbered{margin-left:.625em}
ul.unstyled,ol.unstyled{margin-left:0}
li>p:empty:only-child::before{content:"";display:inline-block}
ul.checklist>li>p:first-child{margin-left:-1em}
ul.checklist>li>p:first-child>.fa-square-o:first-child,ul.checklist>li>p:first-child>.fa-check-square-o:first-child{width:1.25em;font-size:.8em;position:relative;bottom:.125em}
ul.checklist>li>p:first-child>input[type=checkbox]:first-child{margin-right:.25em}
ul.inline{display:flex;flex-flow:row wrap;list-style:none;margin:0 0 .625em -1.25em}
ul.inline>li{margin-left:1.25em}
.unstyled dl dt{font-weight:400;font-style:normal}
ol.arabic{list-style-type:decimal}
ol.decimal{list-style-type:decimal-leading-zero}
ol.loweralpha{list-style-type:lower-alpha}
ol.upperalpha{list-style-type:upper-alpha}
ol.lowerroman{list-style-type:lower-roman}
ol.upperroman{list-style-type:upper-roman}
ol.lowergreek{list-style-type:lower-greek}
.hdlist>table,.colist>table{border:0;background:none}
.hdlist>table>tbody>tr,.colist>table>tbody>tr{background:none}
td.hdlist1,td.hdlist2{vertical-align:top;padding:0 .625em}
td.hdlist1{font-weight:bold;padding-bottom:1.25em}
td.hdlist2{word-wrap:anywhere}
.literalblock+.colist,.listingblock+.colist{margin-top:-.5em}
.colist td:not([class]):first-child{padding:.4em .75em 0;line-height:1;vertical-align:top}
.colist td:not([class]):first-child img{max-width:none}
.colist td:not([class]):last-child{padding:.25em 0}
.thumb,.th{line-height:0;display:inline-block;border:4px solid #fff;box-shadow:0 0 0 1px #ddd}
.imageblock.left{margin:.25em .625em 1.25em 0}
.imageblock.right{margin:.25em 0 1.25em .625em}
.imageblock>.title{margin-bottom:0}
.imageblock.thumb,.imageblock.th{border-width:6px}
.imageblock.thumb>.title,.imageblock.th>.title{padding:0 .125em}
.image.left,.image.right{margin-top:.25em;margin-bottom:.25em;display:inline-block;line-height:0}
.image.left{margin-right:.625em}
.image.right{margin-left:.625em}
a.image{text-decoration:none;display:inline-block}
a.image object{pointer-events:none}
sup.footnote,sup.footnoteref{font-size:.875em;position:static;vertical-align:super}
sup.footnote a,sup.footnoteref a{text-decoration:none}
sup.footnote a:active,sup.footnoteref a:active,#footnotes .footnote a:first-of-type:active{text-decoration:underline}
#footnotes{padding-top:.75em;padding-bottom:.75em;margin-bottom:.625em}
#footnotes hr{width:20%;min-width:6.25em;margin:-.25em 0 .75em;border-width:1px 0 0}
#footnotes .footnote{padding:0 .375em 0 .225em;line-height:1.3334;font-size:.875em;margin-left:1.2em;margin-bottom:.2em}
#footnotes .footnote a:first-of-type{font-weight:bold;text-decoration:none;margin-left:-1.05em}
#footnotes .footnote:last-of-type{margin-bottom:0}
#content #footnotes{margin-top:-.625em;margin-bottom:0;padding:.75em 0}
div.unbreakable{page-break-inside:avoid}
.big{font-size:larger}
.small{font-size:smaller}
.underline{text-decoration:underline}
.overline{text-decoration:overline}
.line-through{text-decoration:line-through}
.aqua{color:#00bfbf}
.aqua-background{background:#00fafa}
.black{color:#000}
.black-background{background:#000}
.blue{color:#0000bf}
.blue-background{background:#0000fa}
.fuchsia{color:#bf00bf}
.fuchsia-background{background:#fa00fa}
.gray{color:#606060}
.gray-background{background:#7d7d7d}
.green{color:#006000}
.green-background{background:#007d00}
.lime{color:#00bf00}
.lime-background{background:#00fa00}
.maroon{color:#600000}
.maroon-background{background:#7d0000}
.navy{color:#000060}
.navy-background{background:#00007d}
.olive{color:#606000}
.olive-background{background:#7d7d00}
.purple{color:#600060}
.purple-background{background:#7d007d}
.red{color:#bf0000}
.red-background{background:#fa0000}
.silver{color:#909090}
.silver-background{background:#bcbcbc}
.teal{color:#006060}
.teal-background{background:#007d7d}
.white{color:#bfbfbf}
.white-background{background:#fafafa}
.yellow{color:#bfbf00}
.yellow-background{background:#fafa00}
span.icon>.fa{cursor:default}
a span.icon>.fa{cursor:inherit}
.admonitionblock td.icon [class^="fa icon-"]{font-size:2.5em;text-shadow:1px 1px 2px rgba(0,0,0,.5);cursor:default}
.admonitionblock td.icon .icon-note::before{content:"\f05a";color:#19407c}
.admonitionblock td.icon .icon-tip::before{content:"\f0eb";text-shadow:1px 1px 2px rgba(155,155,0,.8);color:#111}
.admonitionblock td.icon .icon-warning::before{content:"\f071";color:#bf6900}
.admonitionblock td.icon .icon-caution::before{content:"\f06d";color:#bf3400}
.admonitionblock td.icon .icon-important::before{content:"\f06a";color:#bf0000}
.conum[data-value]{display:inline-block;color:#fff!important;background:rgba(0,0,0,.8);border-radius:50%;text-align:center;font-size:.75em;width:1.67em;height:1.67em;line-height:1.67em;font-family:"Open Sans","DejaVu Sans",sans-serif;font-style:normal;font-weight:bold}
.conum[data-value] *{color:#fff!important}
.conum[data-value]+b{display:none}
.conum[data-value]::after{content:attr(data-value)}
pre .conum[data-value]{position:relative;top:-.125em}
b.conum *{color:inherit!important}
.conum:not([data-value]):empty{display:none}
dt,th.tableblock,td.content,div.footnote{text-rendering:optimizeLegibility}
h1,h2,p,td.content,span.alt,summary{letter-spacing:-.01em}
p strong,td.content strong,div.footnote strong{letter-spacing:-.005em}
p,blockquote,dt,td.content,td.hdlist1,span.alt,summary{font-size:1.0625rem}
p{margin-bottom:1.25rem}
.sidebarblock p,.sidebarblock dt,.sidebarblock td.content,p.tableblock{font-size:1em}
.exampleblock>.content{background:#fffef7;border-color:#e0e0dc;box-shadow:0 1px 4px #e0e0dc}
.print-only{display:none!important}
@page{margin:1.25cm .75cm}
@media print{*{box-shadow:none!important;text-shadow:none!important}
html{font-size:80%}
a{color:inherit!important;text-decoration:underline!important}
a.bare,a[href^="#"],a[href^="mailto:"]{text-decoration:none!important}
a[href^="http:"]:not(.bare)::after,a[href^="https:"]:not(.bare)::after{content:"(" attr(href) ")";display:inline-block;font-size:.875em;padding-left:.25em}
abbr[title]{border-bottom:1px dotted}
abbr[title]::after{content:" (" attr(title) ")"}
pre,blockquote,tr,img,object,svg{page-break-inside:avoid}
thead{display:table-header-group}
svg{max-width:100%}
p,blockquote,dt,td.content{font-size:1em;orphans:3;widows:3}
h2,h3,#toctitle,.sidebarblock>.content>.title{page-break-after:avoid}
#header,#content,#footnotes,#footer{max-width:none}
#toc,.sidebarblock,.exampleblock>.content{background:none!important}
#toc{border-bottom:1px solid #dddddf!important;padding-bottom:0!important}
body.book #header{text-align:center}
body.book #header>h1:first-child{border:0!important;margin:2.5em 0 1em}
body.book #header .details{border:0!important;display:block;padding:0!important}
body.book #header .details span:first-child{margin-left:0!important}
body.book #header .details br{display:block}
body.book #header .details br+span::before{content:none!important}
body.book #toc{border:0!important;text-align:left!important;padding:0!important;margin:0!important}
body.book #toc,body.book #preamble,body.book h1.sect0,body.book .sect1>h2{page-break-before:always}
.listingblock code[data-lang]::before{display:block}
#footer{padding:0 .9375em}
.hide-on-print{display:none!important}
.print-only{display:block!important}
.hide-for-print{display:none!important}
.show-for-print{display:inherit!important}}
@media amzn-kf8,print{#header>h1:first-child{margin-top:1.25rem}
.sect1{padding:0!important}
.sect1+.sect1{border:0}
#footer{background:none}
#footer-text{color:rgba(0,0,0,.6);font-size:.9em}}
@media amzn-kf8{#header,#content,#footnotes,#footer{padding:0}}
</style>
<style>
pre.pygments .hll { background-color: #ffffcc }
pre.pygments { background: #f8f8f8; }
pre.pygments .tok-c { color: #3D7B7B; font-style: italic } /* Comment */
pre.pygments .tok-err { border: 1px solid #F00 } /* Error */
pre.pygments .tok-k { color: #008000; font-weight: bold } /* Keyword */
pre.pygments .tok-o { color: #666 } /* Operator */
pre.pygments .tok-ch { color: #3D7B7B; font-style: italic } /* Comment.Hashbang */
pre.pygments .tok-cm { color: #3D7B7B; font-style: italic } /* Comment.Multiline */
pre.pygments .tok-cp { color: #9C6500 } /* Comment.Preproc */
pre.pygments .tok-cpf { color: #3D7B7B; font-style: italic } /* Comment.PreprocFile */
pre.pygments .tok-c1 { color: #3D7B7B; font-style: italic } /* Comment.Single */
pre.pygments .tok-cs { color: #3D7B7B; font-style: italic } /* Comment.Special */
pre.pygments .tok-gd { color: #A00000 } /* Generic.Deleted */
pre.pygments .tok-ge { font-style: italic } /* Generic.Emph */
pre.pygments .tok-ges { font-weight: bold; font-style: italic } /* Generic.EmphStrong */
pre.pygments .tok-gr { color: #E40000 } /* Generic.Error */
pre.pygments .tok-gh { color: #000080; font-weight: bold } /* Generic.Heading */
pre.pygments .tok-gi { color: #008400 } /* Generic.Inserted */
pre.pygments .tok-go { color: #717171 } /* Generic.Output */
pre.pygments .tok-gp { color: #000080; font-weight: bold } /* Generic.Prompt */
pre.pygments .tok-gs { font-weight: bold } /* Generic.Strong */
pre.pygments .tok-gu { color: #800080; font-weight: bold } /* Generic.Subheading */
pre.pygments .tok-gt { color: #04D } /* Generic.Traceback */
pre.pygments .tok-kc { color: #008000; font-weight: bold } /* Keyword.Constant */
pre.pygments .tok-kd { color: #008000; font-weight: bold } /* Keyword.Declaration */
pre.pygments .tok-kn { color: #008000; font-weight: bold } /* Keyword.Namespace */
pre.pygments .tok-kp { color: #008000 } /* Keyword.Pseudo */
pre.pygments .tok-kr { color: #008000; font-weight: bold } /* Keyword.Reserved */
pre.pygments .tok-kt { color: #B00040 } /* Keyword.Type */
pre.pygments .tok-m { color: #666 } /* Literal.Number */
pre.pygments .tok-s { color: #BA2121 } /* Literal.String */
pre.pygments .tok-na { color: #687822 } /* Name.Attribute */
pre.pygments .tok-nb { color: #008000 } /* Name.Builtin */
pre.pygments .tok-nc { color: #00F; font-weight: bold } /* Name.Class */
pre.pygments .tok-no { color: #800 } /* Name.Constant */
pre.pygments .tok-nd { color: #A2F } /* Name.Decorator */
pre.pygments .tok-ni { color: #717171; font-weight: bold } /* Name.Entity */
pre.pygments .tok-ne { color: #CB3F38; font-weight: bold } /* Name.Exception */
pre.pygments .tok-nf { color: #00F } /* Name.Function */
pre.pygments .tok-nl { color: #767600 } /* Name.Label */
pre.pygments .tok-nn { color: #00F; font-weight: bold } /* Name.Namespace */
pre.pygments .tok-nt { color: #008000; font-weight: bold } /* Name.Tag */
pre.pygments .tok-nv { color: #19177C } /* Name.Variable */
pre.pygments .tok-ow { color: #A2F; font-weight: bold } /* Operator.Word */
pre.pygments .tok-w { color: #BBB } /* Text.Whitespace */
pre.pygments .tok-mb { color: #666 } /* Literal.Number.Bin */
pre.pygments .tok-mf { color: #666 } /* Literal.Number.Float */
pre.pygments .tok-mh { color: #666 } /* Literal.Number.Hex */
pre.pygments .tok-mi { color: #666 } /* Literal.Number.Integer */
pre.pygments .tok-mo { color: #666 } /* Literal.Number.Oct */
pre.pygments .tok-sa { color: #BA2121 } /* Literal.String.Affix */
pre.pygments .tok-sb { color: #BA2121 } /* Literal.String.Backtick */
pre.pygments .tok-sc { color: #BA2121 } /* Literal.String.Char */
pre.pygments .tok-dl { color: #BA2121 } /* Literal.String.Delimiter */
pre.pygments .tok-sd { color: #BA2121; font-style: italic } /* Literal.String.Doc */
pre.pygments .tok-s2 { color: #BA2121 } /* Literal.String.Double */
pre.pygments .tok-se { color: #AA5D1F; font-weight: bold } /* Literal.String.Escape */
pre.pygments .tok-sh { color: #BA2121 } /* Literal.String.Heredoc */
pre.pygments .tok-si { color: #A45A77; font-weight: bold } /* Literal.String.Interpol */
pre.pygments .tok-sx { color: #008000 } /* Literal.String.Other */
pre.pygments .tok-sr { color: #A45A77 } /* Literal.String.Regex */
pre.pygments .tok-s1 { color: #BA2121 } /* Literal.String.Single */
pre.pygments .tok-ss { color: #19177C } /* Literal.String.Symbol */
pre.pygments .tok-bp { color: #008000 } /* Name.Builtin.Pseudo */
pre.pygments .tok-fm { color: #00F } /* Name.Function.Magic */
pre.pygments .tok-vc { color: #19177C } /* Name.Variable.Class */
pre.pygments .tok-vg { color: #19177C } /* Name.Variable.Global */
pre.pygments .tok-vi { color: #19177C } /* Name.Variable.Instance */
pre.pygments .tok-vm { color: #19177C } /* Name.Variable.Magic */
pre.pygments .tok-il { color: #666 } /* Literal.Number.Integer.Long */
</style>
</head>
<body class="article">
<div id="header">
<h1>The rlean-search manual</h1>
<div class="details">
<span id="author" class="author">Nikolaos Chatzikonstantinou</span><br>
<span id="email" class="email"><a href="mailto:nchatz314@gmail.com">nchatz314@gmail.com</a></span><br>
<span id="revdate">0.2.2</span>
</div>
<div id="toc" class="toc">
<div id="toctitle">Table of Contents</div>
<ul class="sectlevel1">
<li><a href="#_introduction">Introduction</a></li>
<li><a href="#_installation">Installation</a></li>
<li><a href="#_usage">Usage</a>
<ul class="sectlevel2">
<li><a href="#_search">Search</a></li>
<li><a href="#_fast_search_with_the_daemon">Fast search with the daemon</a></li>
<li><a href="#_command_line_options">Command-line options</a></li>
</ul>
</li>
</ul>
</div>
</div>
<div id="content">
<div class="sect1">
<h2 id="_introduction">Introduction</h2>
<div class="sectionbody">
<div class="paragraph">
<p>The <code>rlean-search</code> utility is a humble search utility for Lean 4. Its
search functionality is not as good as
<a href="https://loogle.lean-lang.org/">loogle</a>, but it is <strong>much faster</strong>. It was
vibe-coded with Grok Build.</p>
</div>
<div class="paragraph">
<p><code>rlean-search</code> parses the source code of the Lean 4 projects and
produces a cache file that it then loads into memory and runs queries
on. It will probably miss very complicated types; use
<a href="https://loogle.lean-lang.org/">loogle</a> for those.</p>
</div>
<div class="paragraph">
<p>The project repository is
<a href="https://github.com/createyourpersonalaccount/rlean-search">here</a>.</p>
</div>
</div>
</div>
<div class="sect1">
<h2 id="_installation">Installation</h2>
<div class="sectionbody">
<div class="paragraph">
<p><code>rlean-search</code> is written in Rust and uses the Cargo build system. You
can install it for your local user with:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="sh"><span></span>cargo<span class="tok-w"> </span>install<span class="tok-w"> </span>rlean-search</code></pre>
</div>
</div>
</div>
</div>
<div class="sect1">
<h2 id="_usage">Usage</h2>
<div class="sectionbody">
<div class="sect2">
<h3 id="_search">Search</h3>
<div class="sect3">
<h4 id="build-index">Build the index</h4>
<div class="paragraph">
<p>First you must build the index file. For Mathlib, you could do:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="sh"><span></span>rlean-search<span class="tok-w"> </span>index<span class="tok-w"> </span>/path/to/mathlib4</code></pre>
</div>
</div>
<div class="ulist">
<ul>
<li>
<p>This creates a cached index file named <code>index.xml.gz</code> under
<code>/path/to/mathlib4/.rlean-search/</code>.</p>
</li>
<li>
<p>The index file will be created automatically if you attempt to
search without running the above command first.</p>
</li>
<li>
<p>The indexing command is a slow operation, but it only needs to be
run once.</p>
</li>
</ul>
</div>
</div>
<div class="sect3">
<h4 id="_perform_a_search">Perform a search</h4>
<div class="paragraph">
<p>Now you can search Mathlib using:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="sh"><span></span>rlean-search<span class="tok-w"> </span>search<span class="tok-w"> </span>-p<span class="tok-w"> </span>/path/to/mathlib4<span class="tok-w"> </span><span class="tok-s1">'_ + _ = 0'</span></code></pre>
</div>
</div>
<div class="paragraph">
<p>The search mechanism supports:</p>
</div>
<div class="olist arabic">
<ol class="arabic">
<li>
<p>Holes with <code>_</code>.</p>
</li>
<li>
<p>Metavariables with <code>?a</code>.</p>
</li>
<li>
<p>Searching the conclusion with <code>|- tsum _ = _ * tsum _</code>.</p>
</li>
</ol>
</div>
</div>
</div>
<div class="sect2">
<h3 id="_fast_search_with_the_daemon">Fast search with the daemon</h3>
<div class="sect3">
<h4 id="_launch_the_daemon">Launch the daemon</h4>
<div class="paragraph">
<p>Build the <a href="#build-index">index</a> and then run the daemon server:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="sh"><span></span>rlean-search<span class="tok-w"> </span>daemon<span class="tok-w"> </span>/path/to/mathlib4</code></pre>
</div>
</div>
<div class="admonitionblock note">
<table>
<tr>
<td class="icon">
<div class="title">Note</div>
</td>
<td class="content">
The daemon startup will be a little slow, even if the index has been built.
</td>
</tr>
</table>
</div>
<div class="paragraph">
<p>The daemon by default runs on <code>127.0.0.1:7878</code>. Now clients can
communicate with the daemon using either JSON or XML queries.</p>
</div>
</div>
<div class="sect3">
<h4 id="_query_with_rlean_search">Query with <code>rlean-search</code></h4>
<div class="paragraph">
<p>The <code>rlean-search</code> utility provides a client:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="sh"><span></span>rlean-search<span class="tok-w"> </span>query<span class="tok-w"> </span>-p<span class="tok-w"> </span><span class="tok-s1">'_ + _ = 0'</span><span class="tok-w"> </span><span class="tok-p">|</span><span class="tok-w"> </span>jq</code></pre>
</div>
</div>
<div class="paragraph">
<p>You will get the results back <strong>instantly!</strong> (We pipe the result to
<a href="https://jqlang.org/">jq</a> for neat viewing.)</p>
</div>
</div>
<div class="sect3">
<h4 id="_query_with_a_script">Query with a script</h4>
<div class="paragraph">
<p>If you wish to query the daemon from your own script without invoking
<code>rlean-search</code>, follow the steps:</p>
</div>
<div class="olist arabic">
<ol class="arabic">
<li>
<p>Establish a connection to <code>127.0.0.1:7878</code>.</p>
</li>
<li>
<p>Send queries either in JSON or XML.</p>
</li>
<li>
<p>Read the responses.</p>
</li>
</ol>
</div>
<div class="sect4">
<h5 id="_example_query_with_json">Example query with JSON</h5>
<div class="paragraph">
<p>Send the following query:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="json"><span></span><span class="tok-p">{</span><span class="tok-w"> </span><span class="tok-nt">"cmd"</span><span class="tok-p">:</span><span class="tok-w"> </span><span class="tok-s2">"search"</span><span class="tok-p">,</span><span class="tok-w"> </span><span class="tok-nt">"limit"</span><span class="tok-p">:</span><span class="tok-w"> </span><span class="tok-mi">2</span><span class="tok-p">,</span><span class="tok-w"> </span><span class="tok-nt">"pattern"</span><span class="tok-p">:</span><span class="tok-w"> </span><span class="tok-s2">"_ + _ = 0"</span><span class="tok-w"> </span><span class="tok-p">}</span></code></pre>
</div>
</div>
<div class="admonitionblock important">
<table>
<tr>
<td class="icon">
<div class="title">Important</div>
</td>
<td class="content">
The JSON query must be in a single line.
NOTE: For this example we limit the results to only 2.
</td>
</tr>
</table>
</div>
<div class="paragraph">
<p>The response will be a single line like this:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="json"><span></span><span class="tok-p">{</span><span class="tok-nt">"type"</span><span class="tok-p">:</span><span class="tok-s2">"search"</span><span class="tok-p">,</span><span class="tok-nt">"pattern"</span><span class="tok-p">:</span><span class="tok-s2">"_ + _ = 0"</span><span class="tok-p">,</span><span class="tok-nt">"count"</span><span class="tok-p">:</span><span class="tok-mi">2</span><span class="tok-p">,</span><span class="tok-nt">"hits"</span><span class="tok-p">:[{</span><span class="tok-nt">"name"</span><span class="tok-p">:</span><span class="tok-s2">"Odd"</span><span class="tok-p">,</span><span class="tok-nt">"full_name"</span><span class="tok-p">:</span><span class="tok-s2">"Odd"</span><span class="tok-p">,</span><span class="tok-nt">"kind"</span><span class="tok-p">:</span><span class="tok-s2">"lemma"</span><span class="tok-p">,</span><span class="tok-nt">"type_surface"</span><span class="tok-p">:</span><span class="tok-s2">"a ^ n + b ^ n = 0"</span><span class="tok-p">,</span><span class="tok-nt">"file"</span><span class="tok-p">:</span><span class="tok-s2">"/home/grok/mathlib4/Mathlib/Algebra/Ring/Parity.lean"</span><span class="tok-p">,</span><span class="tok-nt">"line"</span><span class="tok-p">:</span><span class="tok-mi">153</span><span class="tok-p">,</span><span class="tok-nt">"score"</span><span class="tok-p">:</span><span class="tok-mi">149</span><span class="tok-p">},{</span><span class="tok-nt">"name"</span><span class="tok-p">:</span><span class="tok-s2">"term"</span><span class="tok-p">,</span><span class="tok-nt">"full_name"</span><span class="tok-p">:</span><span class="tok-s2">"term"</span><span class="tok-p">,</span><span class="tok-nt">"kind"</span><span class="tok-p">:</span><span class="tok-s2">"axiom"</span><span class="tok-p">,</span><span class="tok-nt">"type_surface"</span><span class="tok-p">:</span><span class="tok-s2">"∀ a b : ℚ, a + b = 0"</span><span class="tok-p">,</span><span class="tok-nt">"file"</span><span class="tok-p">:</span><span class="tok-s2">"/home/grok/mathlib4/MathlibTest/Tactic/Grind/Grobner.lean"</span><span class="tok-p">,</span><span class="tok-nt">"line"</span><span class="tok-p">:</span><span class="tok-mi">70</span><span class="tok-p">,</span><span class="tok-nt">"score"</span><span class="tok-p">:</span><span class="tok-mi">147</span><span class="tok-p">}]}</span></code></pre>
</div>
</div>
<div class="admonitionblock note">
<table>
<tr>
<td class="icon">
<div class="title">Note</div>
</td>
<td class="content">
The above command returned a result from Mathlib’s test suite!
You can perform subsequent filtering yourself on the result of the
query, or you can delete the test suite from the Mathlib directory
prior to building the <a href="#build-index">index</a>.
</td>
</tr>
</table>
</div>
</div>
<div class="sect4">
<h5 id="_example_query_with_xml">Example query with XML</h5>
<div class="paragraph">
<p>Send the following query:</p>
</div>
<div class="listingblock">
<div class="content">
<pre class="pygments highlight"><code data-lang="xml"><span></span><span class="tok-nt"><rlean:search</span><span class="tok-w"> </span><span class="tok-na">xmlns:rlean=</span><span class="tok-s">"http://github.com/createyourpersonalaccount/rlean-search"</span><span class="tok-w"> </span><span class="tok-na">pattern=</span><span class="tok-s">"_ + _ = 0"</span><span class="tok-w"> </span><span class="tok-na">limit=</span><span class="tok-s">"50"</span><span class="tok-nt">/></span></code></pre>
</div>
</div>
<div class="admonitionblock important">
<table>
<tr>
<td class="icon">
<div class="title">Important</div>
</td>
<td class="content">
The XML query must be in a single line.
</td>
</tr>
</table>
</div>
<div class="paragraph">
<p>The response will be a multi-line response in XML.</p>
</div>
</div>
</div>
</div>
<div class="sect2">
<h3 id="_command_line_options">Command-line options</h3>
<div class="paragraph">
<p><code>rlean-search</code> follows the command interface that <code>git</code>
popularized. It has the following commands:</p>
</div>
<div class="ulist">
<ul>
<li>
<p><code>index</code></p>
</li>
<li>
<p><code>search</code></p>
</li>
<li>
<p><code>daemon</code></p>
</li>
<li>
<p><code>query</code></p>
</li>
</ul>
</div>
<div class="paragraph">
<p>Use with <code>--help</code> to learn more information about each command, for
instance <code>rlean-search index --help</code>.</p>
</div>
</div>
</div>
</div>
</div>
<div id="footer">
<div id="footer-text">
</div>
</div>
</body>
</html>